proposition: Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
proof: Proof. intros n. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. Qed.
imports: Bool NZAxioms NZMulOrder