proposition: Lemma strictly_increasing_reciprocal_interval_compat : forall f g lb ub, strictly_increasing_interval lb ub f -> reciprocal_interval (f lb) (f ub) f g -> (forall x, interval (f lb) (f ub) x -> interval lb ub (g x)) -> strictly_increasing_interval (f lb) (f ub) g.
proof: Proof. intros f g lb ub f_incr f_recip_g g_ok x y x_in_I y_in_I x_lt_y. destruct (Rlt_le_dec (g x) (g y)) as [T | F]. assumption. destruct F as [F | F]. assert (Hf : y < x). unfold reciprocal_interval, id in f_recip_g ; rewrite <- f_recip_g. apply Rgt_lt ; rewrite <- f_recip_g. unfold comp ; apply f_incr ; [apply g_ok | apply g_ok |] ; assumption. assumption. assumption. apply False_ind ; apply Rlt_irrefl with x ; apply Rlt_trans with y ; assumption. assert (Hf : x = y). unfold reciprocal_interval, id in f_recip_g ; rewrite <- f_recip_g. symmetry ; rewrite <- f_recip_g. unfold comp ; rewrite F ; reflexivity. assumption. assumption. rewrite Hf in x_lt_y ; elim (Rlt_irrefl _ x_lt_y). Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra