proposition: Lemma strictly_increasing_reciprocal_interval_comm: forall f g lb ub, (forall x, interval (f lb) (f ub) x -> interval lb ub (g x)) -> strictly_increasing_interval lb ub f -> reciprocal_interval (f lb) (f ub) f g -> reciprocal_interval lb ub g f.
proof: Proof. intros f g lb ub g_ok f_sinc Hfg x x_in ; assert (f_inc : increasing_interval lb ub f). apply strictly_increasing_in_increasing_in ; assumption. destruct (Req_dec (g (f x)) x) as [Heq | Hneq]. assumption. destruct (Rlt_irrefl (f x)). destruct (Rdichotomy _ _ Hneq) as [Hlt | Hlt]. apply Rle_lt_trans with (f (g (f x))). right ; rewrite Hfg. reflexivity. apply increasing_interval_image ; [apply strictly_increasing_in_increasing_in |] ; assumption. apply f_sinc ; [apply g_ok, increasing_interval_image | |] ; assumption. apply Rlt_le_trans with (f (g (f x))). apply f_sinc ; [| apply g_ok, increasing_interval_image |] ; assumption. right ; rewrite Hfg. reflexivity. apply increasing_interval_image ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra