proposition: Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.
proof: Proof. intros x y ?; unfold Qdiv. rewrite (Qmult_assoc y x (Qinv y)). rewrite (Qmult_comm y x). fold (Qdiv (Qmult x y) y). apply Qdiv_mult_l; auto. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool