proposition: Lemma Rmult_eq_compat_r_rev_strong : forall a b c d, a * c = b * d -> c = d -> d <> 0 -> a = b.
proof: Proof. intros a b c d Heq Hcd c_neq. replace a with (a * c * / c). replace b with (b * d * / d). subst ; apply Rmult_eq_compat_r ; assumption. field ; subst ; assumption. field ; subst ; assumption. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5