20170605.v

Require Import Omega.
Goal ~(exists f : nat -> nat, forall n : nat, f (f n) = n + 1).
Proof.
intro H.
destruct H as [f H].
assert (forall n : nat, f n = n + f 0).
intro n.
induction n.
reflexivity.
simpl.
rewrite <- IHn.
replace (S n) with (n + 1) by omega.
replace (S (f n)) with (f n + 1) by omega.
rewrite <- H.
rewrite <- H.
reflexivity.
specialize (H 0).
rewrite H0 in H.
apply (odd_even_lem 0 (f 0)).
omega.
Qed.