proposition: Lemma Integral_comm_scal : forall c (H : Continuous_I Hab (c{**}F)), Integral H [=] c[*]Integral contF.
proof: Proof. intros. unfold Integral in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply dist_2a. apply cg_minus_wd; apply integral_comm_scal. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions