proposition: Lemma card_rem a P : card (Pf_rem a P) = card P - if dec (mem a P) then 1 else 0.
proof: Proof. destruct (dec (mem a P)). rewrite (Pf_eq_of_list P). set (l := list_of_finite P). set (P' := Pf_of_list l). rewrite (Pf_equiv_of2 (P:=Pf_rem a P') (Q:=Pf_of_list (remove eq_dec a l))). assert (h : nodup l). apply nodup_list_of_finite. unfold P'. rewrite !card_of_list_eq_length, length_remove_nodup; auto. unfold l. rewrite In_list_of_finite. hyp. apply nodup_remove. hyp. simpl. sym. apply of_remove. rewrite Nat.sub_0_r. apply card_equiv. unfold Pf_equiv. simpl. apply rem_notin. hyp. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)