proposition: Theorem divides_div : forall p q : nat, 0 < p -> divides p q -> q = div q p * p.
proof: Proof. intros p q Hp (x, H); rewrite H. apply f_equal2 with (f := mult); auto with arith. apply div_unique; auto with arith. rewrite (Nat.mul_comm x); auto with arith. rewrite (Nat.mul_comm x); auto with arith. Qed.
imports: Coq(ArithRing) Bertrand(Misc)