proposition: Lemma Sum0_comm_scal' : forall (s : nat -> IR) a m, Sum0 m (fun i => a[*]s i) [=] a[*]Sum0 m s.
proof: Proof. intros. apply eq_transitive_unfolded with (Sum0 m s[*]a). 2: astepr (Sum0 m s[*]a); apply mult_wdl. 2: apply Sum0_wd; algebra. eapply eq_transitive_unfolded. 2: apply Sum0_comm_scal. apply Sum0_wd; algebra. Qed.
imports: CoRN.reals.CReals1