proposition: Lemma card_disjoint_union : forall A (E F:set A), finite E -> finite F -> E \# F -> card (E \u F) = (card E + card F)%nat.
proof: Proof. Proof using. introv FE FF EF. forwards: card_union_le FE FF. cuts: (card (E \u F) >= (card E + card F)%nat). math. clear H. forwards (L&LC&LL): finite_inv_list_covers_and_card (E \u F). applys~ finite_union. rewrite LL. clear LL. sets PE: (fun x => x \in E). sets LE: (filter PE L). sets PF: (fun x => x \in F). sets LF: (filter PF L). forwards: list_covers_inv_card E LE. unfold LE, PE. introv Ex. forwards: LC x. set_prove. applys~ mem_filter. forwards: list_covers_inv_card F LF. unfold LF, PF. introv Fx. forwards: LC x. set_prove. applys~ mem_filter. forwards LEF: filter_length_two_disjoint PE PF L. introv _ HEx HFx. unfolds PE, PF. applys* @disjoint_inv. typeclass. subst LE LF. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)