proposition: Lemma Rplus_eq_compat_l_rev_strong : forall a b c d, a + c = b + d -> a = b -> c = d.
proof: Proof. intros a b c d Heq Hab ; replace c with (a + c - a) by ring ; replace d with (b + d - b) by ring ; subst ; apply Rplus_eq_compat_r ; 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