proposition: Theorem EvenMultInv : forall n m : Z, Even (n * m) -> Odd n -> Even m.
proof: Proof. intros n m H H0; case (OddEvenDec m); auto; intros Z1. contradict H; auto with zarith. apply OddNEven, OddMult; easy. Qed.
imports: Reals ZArith List PeanoNat Psatz