proposition: Lemma length_filter_eq_mem_ge_one : forall x l, mem x l -> length (filter (= x) l) >= 1.
proof: Proof. Proof using. intros. unfolds length. forwards~: LibList.length_filter_eq_mem_ge_one. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)