proposition: Lemma card_disjoint_union_single : forall A (E:set A) x, finite E -> x \notin E -> (card (E \u \{x}) = card E + 1)%nat.
proof: Proof. Proof using. intros. replace 1%nat with (card \{x}) by eauto using card_single. applys~ card_disjoint_union. applys finite_single. rewrite disjoint_single_r_eq. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)