proposition: Lemma Sum_comm_scal : forall (s : nat -> IR) a N m, Sum N m (fun i => s i[*]a) [=] Sum N m s [*]a.
proof: Proof. unfold Sum in |- *. unfold Sum1 in |- *. intros. Step_final (Sum0 (S m) s [*]a[-]Sum0 N s [*]a). Qed.
imports: CoRN.reals.CReals1