proposition: Lemma strictly_increasing_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 (Rle_lt_dec a b) as [aleb | blta]. assumption. destruct (Rlt_irrefl (f a)) ; apply Rle_lt_trans with (f b). assumption. apply Hf ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra