proposition: Lemma strictly_increasing_open_interval_order : forall f lb ub a b, open_interval lb ub a -> open_interval lb ub b -> strictly_increasing_open_interval lb ub f -> f a < f b -> a < b.
proof: Proof. intros f lb ub a b a_in b_in Hf Hfafb ; destruct (Rlt_le_dec a b) as [altb | blea]. assumption. destruct blea as [blta | beqa]. destruct (Rlt_irrefl (f a)) ; transitivity (f b). assumption. apply Hf ; assumption. rewrite beqa in Hfafb ; destruct (Rlt_irrefl _ Hfafb). Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra