proposition: Lemma card_S {P n} : card P = S n -> exists a Q, P =f= Pf_add a Q /\ ~mem a Q /\ card Q = n.
proof: Proof. intro e. gen e. unfold card at 1. destruct P as [P P_fin]; simpl. destruct (cdd (card_uniq P_fin)) as [p [f f_bij]]; simpl. intro; subst. destruct (f zero) as [a aP]. ex a (Pf_rem a P_fin). split. unfold Pf_equiv; simpl. rewrite (add_rem eq_dec). refl. hyp. split. apply notin_rem. rewrite card_rem. unfold mk_Pf at 1. rewrite e. destruct (dec (mem a P_fin)). lia. contr. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)