proposition: Lemma Odd_succ : forall n, Odd (S n) <-> Even n.
proof: Proof. split; intros (m,H). - exists m. apply succ_inj. now rewrite add_1_r in H. - exists m. rewrite add_1_r. now f_equiv. Qed.
imports: Bool NZAxioms NZMulOrder