proposition: Lemma Continuous_I_recip : Continuous_I Hab {1/}G.
proof: Proof. clear incF incG. elim contG; intros incG' contG'. split. Included; assumption. elim Hg'; intros Haux Hg2. elim Hg2; clear Haux Hg2; intros c H H0. intros. elim contG' with (c[*]c[*]e); clear contG contG'. intros d H2 H3. exists d. assumption. intros x y H4 H5 Hx Hy H6. simpl in |- *. set (Hxx := incG' x H4) in *. set (Hyy := incG' y H5) in *. apply leEq_wdl with (AbsIR (G y Hyy[-]G x Hxx[/] _[//] mult_resp_ap_zero _ _ _ (Hg'' x Hxx H4) (Hg'' y Hyy H5))). apply leEq_wdl with (AbsIR (G y Hyy[-]G x Hxx) [/] _[//] AbsIR_resp_ap_zero _ (mult_resp_ap_zero _ _ _ (Hg'' x Hxx H4) (Hg'' y Hyy H5))). apply leEq_transitive with (AbsIR (G y Hyy[-]G x Hxx) [/] _[//] mult_resp_ap_zero _ _ _ (pos_ap_zero _ _ H) (pos_ap_zero _ _ H)). rstepl (AbsIR (G y Hyy[-]G x Hxx) [*] ([1][/] _[//] AbsIR_resp_ap_zero _ (mult_resp_ap_zero _ _ _ (Hg'' x Hxx H4) (Hg'' y Hyy H5)))). rstepr (AbsIR (G y Hyy[-]G x Hxx) [*] ([1][/] _[//] mult_resp_ap_zero _ _ _ (pos_ap_zero _ _ H) (pos_ap_zero _ _ H))). apply mult_resp_leEq_lft. apply recip_resp_leEq. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; assumption. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try (apply less_leEq; assumption). eapply leEq_wdr; [ apply (H0 x Hxx H4) | algebra ]. eapply leEq_wdr; [ apply (H0 y Hyy H5) | algebra ]. apply AbsIR_nonneg. apply shift_div_leEq'. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; assumption. eapply leEq_wdl. 2: apply AbsIR_minus. apply H3; assumption. apply eq_symmetric_unfolded; apply AbsIR_division. apply AbsIR_wd. rational. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; assumption. assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac