proposition: Lemma Continuous_I_mult : Continuous_I Hab (F{*}G).
proof: Proof. clear incF incG. elim contF; intros incF' contF'. elim contG; intros incG' contG'. split; [ Included | intros e H ]. cut {xf : IR | forall (x : IR) (Hx : I x) (Hx' : P x), AbsIR (F x Hx') [<=] xf}. cut {xg : IR | forall (x : IR) (Hx : I x) (Hx' : Q x), AbsIR (G x Hx') [<=] xg}. 2: unfold I, Q in |- *; apply Continuous_I_imp_abs_lub; assumption. 2: unfold I, P in |- *; apply Continuous_I_imp_abs_lub; assumption. intros H0 H1. elim H0; clear H0; intros x H2. elim H1; clear H1; intros x0 H0. elim (contF' (e [/]TwoNZ[/] Max x [1][//]max_one_ap_zero _)); clear contF. elim (contG' (e [/]TwoNZ[/] Max x0 [1][//]max_one_ap_zero _)); clear contG. intros dg H1 H3 df H4 H5. 2: apply div_resp_pos. 2: apply pos_max_one. 2: apply pos_div_two; assumption. 2: apply div_resp_pos. 2: apply pos_max_one. 2: apply pos_div_two; assumption. exists (Min df dg). apply less_Min; assumption. intros; simpl in |- *. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). apply leEq_wdl with (AbsIR (F x1 (ProjIR1 Hx) [*] (G x1 (ProjIR2 Hx) [-]G y (ProjIR2 Hy)) [+] (F x1 (ProjIR1 Hx) [-]F y (ProjIR1 Hy)) [*]G y (ProjIR2 Hy))). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (x0[*]AbsIR (G x1 (ProjIR2 Hx) [-]G y (ProjIR2 Hy))). apply mult_resp_leEq_rht. apply H0; assumption. apply AbsIR_nonneg. apply leEq_transitive with (Max x0 [1][*]AbsIR (G x1 (ProjIR2 Hx) [-]G y (ProjIR2 Hy))). apply mult_resp_leEq_rht; [ apply lft_leEq_Max | apply AbsIR_nonneg ]. astepl (AbsIR (G x1 (ProjIR2 Hx) [-]G y (ProjIR2 Hy)) [*]Max x0 [1]). apply shift_mult_leEq with (max_one_ap_zero x0); [ apply pos_max_one | simpl in |- *; apply H3 ]; try assumption. apply leEq_transitive with (Min df dg); [ assumption | apply Min_leEq_rht ]. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (AbsIR (F x1 (ProjIR1 Hx) [-]F y (ProjIR1 Hy)) [*]x). apply mult_resp_leEq_lft; [ apply H2 | apply AbsIR_nonneg ]; assumption. apply leEq_transitive with (AbsIR (F x1 (ProjIR1 Hx) [-]F y (ProjIR1 Hy)) [*]Max x [1]). apply mult_resp_leEq_lft; [ apply lft_leEq_Max with (y := OneR) | apply AbsIR_nonneg ]. apply shift_mult_leEq with (max_one_ap_zero x); [ apply pos_max_one | simpl in |- *; apply H5 ]; try assumption. apply leEq_transitive with (Min df dg); [ assumption | apply Min_leEq_lft ]. apply AbsIR_wd; rational. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac