proposition: Lemma count_eq_length_filter : forall P l, count P l = length (filter P l).
proof: Proof. Proof using. gowith LibList.count_eq_length_filter. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)