proposition: Lemma card_union_le : forall A (E F:set A), finite E -> finite F -> card (E \u F) <= (card E + card F)%nat.
proof: Proof. Proof using. introv FE FF. lets (LE&RE&QE): finite_inv_list_covers_and_card FE. lets (LF&RF&QF): finite_inv_list_covers_and_card FF. lets H: list_covers_inv_card (E \u F) (LE++LF) __. unfolds list_covers. intros. apply mem_app. rewrite in_union_eq in H. autos*. rew_list in H. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)