proposition: Lemma Sum0_comm_scal : forall (s : nat -> IR) a m, Sum0 m (fun i => s i[*]a) [=] Sum0 m s [*]a.
proof: Proof. intros. induction m as [| m Hrecm]; intros. simpl in |- *. algebra. simpl in |- *. Step_final (Sum0 m s [*]a[+]s m[*]a). Qed.
imports: CoRN.reals.CReals1