proposition: Lemma card_le_of_incl : forall A (E F:set A), finite F -> E \c F -> (card E <= card F)%nat.
proof: Proof. Proof using. introv FF CF. lets FE: finite_incl CF FF. lets (LF&RF&QF): finite_inv_list_covers_and_card FF. rewrite QF. applys list_covers_inv_card. introv Ex. applys RF. applys* @incl_inv. typeclass. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)