proposition: Lemma Integral_minus : 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_minus. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions