CoqEx14.v

Require Import Arith.
Theorem FF : ~exists f, forall n, f (f n) = S n.
Proof.
intro.
destruct H.
remember (x 0) as y.
assert( forall k, x (y + k) = S k ).
induction k.
rewrite <- (plus_n_O y).
rewrite Heqy.
rewrite (H 0).
reflexivity.
remember (y + S k).
rewrite <- H.
apply f_equal.
subst n.
rewrite NPeano.Nat.add_succ_r.
rewrite <- (H (y + k)).
apply f_equal.
apply IHk.
destruct y.
assert (0 = 1).
rewrite <- H.
rewrite <- Heqy.
apply Heqy.
discriminate.
assert (0 = S y + y).
apply eq_add_S.
rewrite <- (H 0).
rewrite <- Heqy.
rewrite <- (H (S y + y)).
rewrite (H0 y).
reflexivity.
discriminate.
Qed.