proposition: Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
proof: Proof. split; intros (m,H). - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). - destruct m as [|m]; try discriminate. exists m. simpl in H; rewrite <- plus_n_Sm in H. inversion H; simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass