proposition: Lemma Sum_comm_scal' : forall (s : nat -> IR) a m n, Sum m n (fun i => a[*]s i) [=] a[*]Sum m n s.
proof: Proof. intros. unfold Sum, Sum1 in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply dist_2a. apply cg_minus_wd; apply Sum0_comm_scal'. Qed.
imports: CoRN.reals.CReals1