proposition: Lemma Rmult_Rdiv: forall x y z t : R, z <> R0 -> t <> R0 -> x * t = y * z -> x / z = y / t.
proof: Proof. intros x y z t Hz Ht Hxtyz; apply Rmult_reg_l with (z*t); auto; transitivity (x*t); [|transitivity (y*z); trivial]; field; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)