proposition: Lemma negb_odd : forall n, negb (odd n) = even n.
proof: Proof. intros n. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. destruct (odd n), (even n) ; simpl; intuition. Qed.
imports: Bool NZAxioms NZMulOrder