proposition: Lemma sigma_mult : forall (f : nat -> U) n c, retract f n -> sigma (fun k => c * (f k)) n == c * (sigma f n).
proof: Proof. intros; induction n; simpl; auto. repeat rewrite sigma_S. assert (H1: retract f n); auto. rewrite (IHn H1). rewrite (Udistr_plus_left c _ _ (retractS H)); auto. Qed.
imports: ALEA(Utheory)