proposition: Lemma integral_comm_scal : forall (c : IR) Hf', Integral (c{**}F) Hf' [=] c[*]Integral F contF.
proof: Proof. intros. apply eq_transitive_unfolded with (Lim (Cauchy_const c) [*]Integral F contF); unfold integral in |- *. eapply eq_transitive_unfolded. 2: apply Lim_mult. apply Lim_wd'; intro; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. eapply eq_transitive_unfolded. 2: apply Sumx_comm_scal'. apply Sumx_wd; intros; simpl in |- *; rational. apply mult_wdl. apply eq_symmetric_unfolded; apply Lim_const. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)