fact: Definition _BagInsertCount := forall (search_term : SearchTermType) (item : TItem) (container : BagType), RepInv container -> _bcount (binsert container item) search_term = _bcount container search_term + if bfind_matcher search_term item then 1 else 0.
imports: Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms