proposition: Lemma Qmult_reg_l: forall x y z: Q, z <> Zero -> z*x = z*y -> x=y.
proof: Proof. intros x y z Hz Hzxy; apply Qminus_Qeq; assert (H:z*(x-y)=Zero); [ transitivity (z*x-z*y); [ ring | apply Qeq_Qminus; auto ] | case (Q_integral _ _ H); trivial; intro H'; contradiction ]. Qed.