proposition: Lemma Integral_wd : Feq (Compact Hab) F G -> Integral contF [=] Integral contG.
proof: Proof. intros; unfold Integral in |- *. apply cg_minus_wd; apply integral_wd. apply included_Feq with (Compact Hab). apply compact_inc_Min_rht. assumption. apply included_Feq with (Compact Hab). apply compact_inc_Min_lft. assumption. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions