proposition: Lemma card_0 {P} : card P = 0 -> P =f= Pf_empty.
proof: Proof. unfold card. destruct P as [P P_fin]. destruct (cdd (card_uniq P_fin)) as [n [f [f_inj f_surj]]]. intro; subst. unfold Pf_equiv; simpl. intro x. split. 2: fo. intro hx. destruct (f_surj (elt hx)) as [k _]. destruct k. lia. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)