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