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