proposition: Lemma odd_add_mul_even : forall n m p, Even m -> odd (n+m*p) = odd n.
proof: Proof. intros n m p Hm. apply even_spec in Hm. apply odd_add_even. apply even_spec. now rewrite even_mul, Hm. Qed.
imports: Bool NZAxioms NZMulOrder