proposition: Lemma Ropp_eq_compat_rev : forall a b, - a = - b -> a = b.
proof: Proof. intros a b Heq ; rewrite <- Ropp_involutive, <- Heq, Ropp_involutive ; reflexivity. 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