proposition: Lemma Rmin_lt_Rmax : forall a b, a <> b -> Rmin a b < Rmax a b.
proof: Proof. intros a b Hneq ; unfold Rmin, Rmax ; destruct (Rle_dec a b). apply Rneq_le_lt ; assumption. apply Rnot_le_lt ; 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