proposition: Lemma continuity_reciprocal_strictly_decreasing_open_interval : forall (f g:R->R) (lb ub:R), lb <= ub -> strictly_decreasing_interval lb ub f -> reciprocal_interval lb ub g f -> continuity_interval lb ub f -> continuity_open_interval (f ub) (f lb) g.
proof: Proof. intros f g lb ub lb_le_ub f_incr Hfg Hf ; apply continuity_open_interval_Ropp_compat_rev. apply (continuity_reciprocal_strictly_increasing_open_interval (- f)%F). assumption. apply strictly_decreasing_in_opp ; assumption. apply reciprocal_opp_compat_interval ; assumption. apply continuity_in_opp ; 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