proposition: Theorem divides_mult : forall a b c d : nat, divides a c -> divides b d -> divides (a * b) (c * d).
proof: Proof. intros a b c d (q1, H) (q2, H0); exists (q1 * q2); rewrite H; rewrite H0; ring. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)