proposition: Lemma Rdiv_eq_reg a b c d : (a * d = b * c -> b <> 0%R -> d <> 0%R -> a / b = c / d)%R.
proof: Proof. intros Heq Hb Hd. apply (Rmult_eq_reg_r (b * d)). field_simplify; trivial. try now rewrite Heq. now apply Rmult_neq0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot