proposition: Lemma Integral_strext : Integral contF [#] Integral contG -> {x : IR | Compact Hab x | forall Hx Hx', Part F x Hx [#] Part G x Hx'}.
proof: Proof. intro H. unfold Integral in H. elim (cg_minus_strext _ _ _ _ _ H); intro. elim (integral_strext _ _ _ _ _ _ _ a0); intros. exists x. apply compact_inc_Min_rht with (H := Min_leEq_rht a b); assumption. assumption. elim (integral_strext _ _ _ _ _ _ _ b0); intros. exists x. apply compact_inc_Min_lft with (H := Min_leEq_lft a b); assumption. assumption. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions