proposition: Lemma Continuous_prim : Continuous J G.
proof: Proof. split. Included. intros a b Hab H. split. Included. intros e H0. simpl in |- *; simpl in H. exists (e[/] _[//] max_one_ap_zero (Norm_Funct (included_imp_Continuous _ _ contF _ _ _ H))). apply div_resp_pos. apply pos_max_one. assumption. intros x y H1 H2 Hx Hy H3. cut (included (Compact (Min_leEq_Max y x)) (Compact Hab)). intro Hinc. cut (Continuous_I (Min_leEq_Max y x) F). intro H4. apply leEq_wdl with (AbsIR (Integral H4)). eapply leEq_transitive. apply Integral_leEq_norm. apply leEq_transitive with (Max (Norm_Funct (included_imp_Continuous _ _ contF _ _ _ H)) [1][*] AbsIR (x[-]y)). apply mult_resp_leEq_rht. apply leEq_transitive with (Norm_Funct (included_imp_Continuous _ _ contF _ _ _ H)). apply leEq_Norm_Funct. intros. apply norm_bnd_AbsIR. apply Hinc; auto. apply lft_leEq_Max. apply AbsIR_nonneg. eapply shift_mult_leEq'. apply pos_max_one. apply H3. apply AbsIR_wd. rstepl (Integral (prim_lemma J F contF x0 Hx0 y Hy) [+]Integral H4[-] Integral (prim_lemma J F contF x0 Hx0 y Hy)). apply cg_minus_wd. apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 x0 x y). apply included_imp_Continuous with J; auto. apply included3_interval; auto. apply Integral_wd. apply Feq_reflexive. apply (included_trans _ (Compact (Min_leEq_Max x0 y)) J); Included. apply included_imp_Continuous with J; auto. Included. Included. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems