proposition: Lemma Rdiv_Rmult_numerator_denominator: forall x y z t: R, t <> 0%R -> y <> 0%R -> ((x/y)*(z/t))%R=((x*z)/(y*t))%R.
proof: Proof. intros; field; auto. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)