proposition: Lemma even_mul : forall n m, even (mul n m) = even n || even m.
proof: Proof. intros n m. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. + intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). + rewrite <- !negb_true_iff, !negb_even, !odd_spec. intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. now rewrite add_shuffle1, add_assoc, !mul_assoc. Qed.
imports: Bool NZAxioms NZMulOrder