proposition: Lemma card_diff_single : forall A (E:set A) x, finite E -> x \in E -> (card (E \-- x) = card E - 1)%nat.
proof: Proof. Proof using. intros. assert (h1: (E \-- x) \u \{x} = E). { rewrite union_comm. erewrite eq_union_single_remove_one by eauto. reflexivity. } forwards h2: card_disjoint_union_single (E \-- x) x. { eauto with finite. } { unfold notin. rewrite set_in_remove_eq. rew_logic. right. eapply in_single_self. } rewrite h1 in h2. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)