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