proposition: Lemma sigma_fin_mult : forall (f : A -> U) c (P:A->Prop)(FP:finite P), retract_fin P f -> sigma_fin (fun k => c * f k) FP == c * sigma_fin f FP.
proof: Proof. induction FP; simpl; intros. repeat Usimpl; auto. assert (incl Q P). apply incl_trans with (add x Q); auto. rewrite Udistr_plus_left; auto. rewrite IHFP; auto. apply retract_fin_incl with P; auto. apply H; auto. case (e x); intuition. Qed.
imports: ALEA(Utheory) ALEA(Sets)