proposition: Lemma cover_incl_fle : forall (A:Type)(P Q:set A)(f g:MF A), cover P f -> cover Q g -> incl P Q -> f <= g.
proof: Proof. intros; intro x. apply (cover_elim H x); auto; intros (Hp,Hfeq). rewrite Hfeq; auto. rewrite (cover_eq_one x H0); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)