proposition: Lemma Rlt_plus_exchange : forall a b c, a - b < c -> a < b + c.
proof: Proof. intros a b c H ; lra. Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv