proposition: Lemma CountingListAsBag_Partition_App (container : CountingList) (search_term : TItem -> bool) (cconsistent : CountingList_RepInv container) : length (let (g, d) := CountingListPartition (ccontents container) search_term in ccontents d ++ ccontents g) = let (g, d) := CountingListPartition (ccontents container) search_term in (clength g) + (clength d).
proof: Proof. unfold CountingList_RepInv in *. destruct container as [n l]; simpl; revert n cconsistent; induction l; simpl; intros; eauto. destruct (search_term a); simpl; destruct (CountingListPartition l search_term); simpl. erewrite <- IHl, !List.app_length; simpl; auto with arith. erewrite IHl; auto with arith. simpl; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts