proposition: Lemma strictly_decreasing_reciprocal_interval_comm: forall f g lb ub, (forall x, interval (f ub) (f lb) x -> interval lb ub (g x)) -> strictly_decreasing_interval lb ub f -> reciprocal_interval (f ub) (f lb) f g -> reciprocal_interval lb ub g f.
proof: Proof. intros f g lb ub g_ok f_sdec Hfg x x_in ; assert (f_dec : decreasing_interval lb ub f). apply strictly_decreasing_in_decreasing_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 Rlt_le_trans with (f (g (f x))). apply f_sdec ; [apply g_ok, decreasing_interval_image | |] ; assumption. right ; rewrite Hfg. reflexivity. apply decreasing_interval_image ; assumption. apply Rle_lt_trans with (f (g (f x))). right ; rewrite Hfg. reflexivity. apply decreasing_interval_image ; assumption. apply f_sdec ; [| apply g_ok, decreasing_interval_image |] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra