proposition: Lemma List_BagCountCorrect : BagCountCorrect ListBag_RepInv ListAsBag_bcount ListAsBag_bfind.
proof: Proof. unfold BagCountCorrect, ListAsBag_bcount, ListAsBag_bfind; intros; pose proof (List_BagCountCorrect_aux container search_term 0) as temp; rewrite Nat.add_0_r in temp; simpl in temp; exact temp. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.ZArith.ZArith