proposition: Lemma _binsert_count : _BagInsertCount.
proof: Proof. unfold _BagInsertCount, _bcount; intros; rewrite binsert_enumerate; simpl; destruct (bfind_matcher search_term item); simpl; eauto. rewrite Nat.add_comm; reflexivity. Qed.
imports: Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms