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