proposition: Lemma Forall_not_eq_count_eq_zero : forall P l, Forall (fun x => ~ P x) l = (count P l = 0).
proof: Proof. Proof using. intros. induction l; rew_listx. { extens*. } { rewrite IHl. extens. iff (M1&M2) M; case_if. { math. } { false. math. } { split~. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)