proposition: Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.
proof: Proof. intros x y H; unfold Qdiv. rewrite <- (Qmult_assoc x y (Qinv y)). rewrite (Qmult_inv_r y H). apply Qmult_1_r. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool