proposition: Lemma List_BagCountCorrect_aux : forall (container: list TItem) (search_term: TSearchTerm) default, length (List.filter (bfind_matcher search_term) container) + default = List.fold_left (fun (acc : nat) (x : TItem) => acc + (if bfind_matcher search_term x then 1 else 0)) container default.
proof: Proof. induction container; intros. + trivial. + simpl; destruct (bfind_matcher search_term a); simpl; rewrite <- IHcontainer; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.ZArith.ZArith