proposition: Lemma Rdiv_Rdiv_Rmult_numerator: forall x y z : R, y <> 0 -> z <> 0 -> (x / y / z) = (x / (y * z)).
proof: Proof. intros x y z Hy Hz; field; split; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)