proposition: Lemma sigma_prod_ge : forall (f g : nat -> U) (c:U), (forall k, c <= (f k)) -> forall n, (retract g n) -> c * (sigma g n) <= (sigma (fun k => (f k) * (g k)) n).
proof: Proof. induction n; simpl; intros; auto. repeat rewrite sigma_S. rewrite (Udistr_plus_left c _ _ (retractS H0)); auto. apply Ole_trans with (c * (g n) + sigma (fun k : nat => f k * g k) n); auto. Qed.
imports: ALEA(Utheory)