proposition: Lemma length_filter_eq_mem_ge_one : forall x l, mem x l -> length (filter (= x) l) >= 1.
proof: Proof. Proof using. introv M. induction l. { inverts M. } { rewrite filter_cons. case_if. { rew_list. nat_math. } { inverts M. false. applys~ IHl. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)