proposition: Lemma derive_pt_recip_interv_prelim1_0 : forall f g lb ub x, lb <= ub -> open_interval (f lb) (f ub) x -> strictly_increasing_interval lb ub f -> (forall x : R, interval (f lb) (f ub) x -> interval lb ub (g x)) -> reciprocal_interval (f lb) (f ub) f g -> open_interval lb ub (g x).
proof: Proof. intros f g lb ub x lb_lt_ub x_in_I f_incr g_ok f_recip_g ; assert (f lb <= f ub). eapply strictly_increasing_in_increasing_in ; [| apply interval_l | apply interval_r |] ; assumption. assert (Hrew := strictly_increasing_reciprocal_interval_comm f g lb ub g_ok f_incr f_recip_g) ; assert (g_incr := strictly_increasing_reciprocal_interval_compat _ _ _ _ f_incr f_recip_g g_ok). split ; unfold reciprocal_interval, comp, id in Hrew ; [rewrite <- (Hrew lb) | rewrite <- Hrew]. apply g_incr ; [apply interval_l | apply open_interval_interval | apply (proj1 x_in_I)] ; assumption. apply interval_l ; assumption. apply g_incr ; [apply open_interval_interval | apply interval_r | apply (proj2 x_in_I)] ; assumption. apply interval_r ; assumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def Rseries_def Lra RiemannInt SeqProp PeanoNat RIneq MyRIneq Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval RIVT