proposition: Lemma Integral_integral : forall Hab' HF', Integral [=] integral a b Hab' F HF'.
proof: Proof. intros. unfold Integral in |- *. astepr (integral a b Hab' F HF'[-][0]). apply cg_minus_wd. apply integral_wd'. apply leEq_imp_Min_is_lft; assumption. algebra. apply integral_empty. apply leEq_imp_Min_is_lft; assumption. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions