proposition: Lemma sigma_fin_monotonic : forall (f g : A -> U)(P:A->Prop)(FP:finite P), (forall x, P x -> (f x)<=(g x))-> sigma_fin f FP <= sigma_fin g FP.
proof: Proof. induction FP; simpl; intros; auto. apply Ole_trans with (f x + sigma_fin g FP); repeat Usimpl. apply IHFP. intros; case (e x0); unfold add in *; intuition. apply H; case (e x); unfold add in *; intuition. Qed.
imports: ALEA(Utheory) ALEA(Sets)