proposition: Theorem OddMult : forall n m : Z, Odd n -> Odd m -> Odd (n * m).
proof: Proof. intros n m H1 H2; case H1; case H2; intros z1 Hz1 z2 Hz2; exists (2 * z1 * z2 + z1 + z2)%Z; rewrite Hz1; rewrite Hz2; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz