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