proposition: Lemma Qdiv_Qmult: forall x y z t : Q, z <> Zero -> t <> Zero -> x / z = y / t -> x * t = y * z.
proof: Proof. intros x y z t Hz Ht Hxtyz; apply Qmult_reg_l with ((Qinv z)*(Qinv t)); auto; transitivity (x/z); [ | transitivity (y/t); trivial]; field; auto. Qed.