proposition: Lemma pred_count_eq_1_inv : forall (A : Set)(eqd : eq_dec A)(P : A -> Prop)(ls : list A) c a, pred_count P ls c -> NoDup ls -> P a -> In a ls -> (forall a', In a' ls -> a <> a' -> ~P a') -> c = (S O).
proof: Proof. intuition. assert (pred_count P (a :: (removeFirst eqd ls a)) c). eapply pred_count_permutation. eapply removeFirst_permutation. trivial. trivial. inversion H4; clear H4; subst. assert (n = 0)%nat. eapply pred_count_eq_none_inv. eauto. intuition. eapply H3. eapply removeFirst_in_iff. eauto. assert (~In a (removeFirst eqd ls a)). eapply removeFirst_NoDup_not_in. trivial. intuition; subst; intuition. trivial. lia. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation