proposition: Lemma retract_fin_le : forall (P:A->Prop) (f g:A->U), (forall x, P x -> f x <= g x) -> retract_fin P g -> retract_fin P f.
proof: Proof. unfold retract_fin; intros. apply Ole_trans with (g x); auto. apply Ole_trans with ([1-] sigma_fin g FQ); auto. apply Uinv_le_compat. apply sigma_fin_monotonic; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)