proposition: Lemma Integral_op : forall Hab' (contF' : Continuous_I (a:=Min b a) (b:=Max b a) Hab' F), Integral contF [=] [--] (Integral contF').
proof: Proof. intros. apply cg_inv_unique'. cut (Continuous_I (Min_leEq_Max a a) F). intro H. apply eq_transitive_unfolded with (Integral H). cut (Min (Min a a) b [<=] Max (Max a a) b); intros. apply eq_symmetric_unfolded; apply Integral_plus_Integral with H0. cut (included (Compact H0) (Compact Hab)). intro H1. exact (included_imp_contin _ _ _ _ _ _ _ H1 contF). apply included_compact. split. apply leEq_Min. apply leEq_transitive with a. apply Min_leEq_lft. apply eq_imp_leEq; apply eq_symmetric_unfolded; apply Min_id. apply Min_leEq_rht. apply leEq_transitive with b. apply Min_leEq_rht. apply rht_leEq_Max. split. apply leEq_transitive with b. apply Min_leEq_rht. apply rht_leEq_Max. apply Max_leEq. apply leEq_wdl with a. apply lft_leEq_Max. apply eq_symmetric_unfolded; apply Max_id. apply rht_leEq_Max. apply leEq_transitive with b. apply Min_leEq_rht. apply rht_leEq_Max. apply Integral_empty; algebra. apply included_imp_contin with (Hab := Hab). 2: apply contF. intros x H. apply compact_wd with a. split. apply Min_leEq_lft. apply lft_leEq_Max. inversion_clear H. apply leEq_imp_eq. eapply leEq_wdl. apply H0. apply Min_id. eapply leEq_wdr. apply H1. apply Max_id. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions