proposition: Lemma Pcard_of_inf_spec (P : Pinf W) : forall n, exists X : Pf A, X [<=] P /\ card X = S n.
proof: Proof. induction n. destruct (infinite_not_empty P) as [a aP]. ex (Pf_singleton a). split. 2: apply card_singleton. simpl. intro x. unfold impl. fo. subst. fo. destruct IHn as [X [XP cX]]. set (Q := diff P X). assert (Qinf : infinite Q). unfold Q. apply infinite_diff_finite. intro x. apply dec. destruct P as [P [Pall Pinf]]. hyp. destruct X as [X Xfin]; hyp. destruct (infinite_not_empty Qinf) as [a aQ]. ex (Pf_add a X). split. simpl. intro x. unfold impl. fo. subst. fo. rewrite card_add, cX. destruct (dec (mem a X)). fo. lia. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)