proposition: Lemma Integral_plus : forall H : Continuous_I Hab (F{+}G), Integral H [=] Integral contF[+]Integral contG.
proof: Proof. intro. unfold Integral in |- *. cut (forall x y z w : IR, x[-]y[+] (z[-]w) [=] x[+]z[-] (y[+]w)); intros. 2: rational. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply H0. apply cg_minus_wd; apply integral_plus. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions