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