proposition: Lemma continuity_reciprocal_strictly_monotonous_open_interval : forall (f g:R->R) (lb ub:R), lb <= ub -> strictly_monotonous_interval lb ub f -> reciprocal_interval lb ub g f -> continuity_interval lb ub f -> continuity_open_interval (Rmin (f lb) (f ub)) (Rmax (f lb) (f ub)) g.
proof: Proof. intros f g lb ub lb_le_ub f_mono f_eq_g f_cont_interv. destruct f_mono as [f_decr | f_incr]. erewrite decreasing_in_Rmax_simpl, decreasing_in_Rmin_simpl ; try (eapply strictly_decreasing_in_decreasing_in ; eassumption) ; try (apply interval_l || apply interval_r) ; try eassumption ; apply continuity_reciprocal_strictly_decreasing_open_interval ; assumption. erewrite increasing_in_Rmax_simpl, increasing_in_Rmin_simpl ; try (eapply strictly_increasing_in_increasing_in ; eassumption) ; try (apply interval_l || apply interval_r) ; try eassumption ; apply continuity_reciprocal_strictly_increasing_open_interval ; 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