proposition: Lemma integral_plus_Integral : forall a b Hab F c Hac Hcb Hab' Hac' Hcb', integral c b Hcb F Hcb' [=] integral a b Hab F Hab'[-]integral a c Hac F Hac'.
proof: Proof. intros. rstepl (integral a c Hac F Hac'[+]integral c b Hcb F Hcb'[-]integral a c Hac F Hac'). apply cg_minus_wd. apply integral_plus_integral. algebra. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions