proposition: Theorem divides_mult2 : forall a b c : nat, 0 < c -> divides (c * a) (c * b) -> divides a b.
proof: Proof. intros a b c H (r, H1); exists r. apply eq_mult with c; auto with arith. apply Nat.neq_0_lt_0; auto. rewrite H1; ring. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)