proposition: Lemma card_add a P : card (Pf_add a P) = card P + if dec (mem a P) then 0 else 1.
proof: Proof. destruct (dec (mem a P)). rewrite <- plus_n_O. apply card_equiv. apply Pf_equiv_of; simpl. apply add_already_in. hyp. rewrite (Pf_eq_of_list P). set (l := list_of_finite P). set (P' := Pf_of_list l). rewrite (Pf_equiv_of2 (P:=Pf_add a P') (Q:=Pf_of_list (a::l))). rewrite card_of_list_eq_length. simpl length. unfold P', l. rewrite <- Pf_eq_of_list, <- card_eq. lia. simpl. split. unfold l. rewrite In_list_of_finite. hyp. apply nodup_list_of_finite. simpl. sym. apply of_cons. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)