proposition: Lemma RangeTreeBag_btraverse_right_nodup : forall container keys, NoDupA (@eq_key _) (RangeTreeBag_btraverse_right container.(this) keys).
proof: Proof. intros [ ctn_raw ctn_proof ] key. induction ctn_raw. - constructor. - simpl. inversion ctn_proof. subst. specialize (IHctn_raw1 H3). specialize (IHctn_raw2 H5). destruct (Range_Value_le_Max k key). + apply NoDupA_app; try apply eqk_equiv; try apply NoDupA_cons; auto; unfold not; intros. * change ctn_raw1 with {| this := ctn_raw1; is_bst := H3 |}.(this). apply RangeTreeBag_bcollect_nodup. * apply InA_eqk_eqke in H; destruct H. change ctn_raw2 with {| this := ctn_raw2; is_bst := H5 |}.(this) in H. rewrite RangeTreeBag_btraverse_right_correct in H; destruct H. apply Raw.Proofs.MapsTo_In in H; specialize (H7 _ H). apply Raw.Proofs.MX.lt_antirefl in H7; eauto. * change ctn_raw1 with {| this := ctn_raw1; is_bst := H3 |}.(this) in H. destruct x as [ x_key x_bag ]. apply InA_eqk_eqke in H; destruct H. apply InA_eqk_eqke in H0; destruct H0. rewrite RangeTreeBag_bcollect_correct in H; apply Raw.Proofs.MapsTo_In in H; specialize (H6 _ H). inversion H0; clear H0; subst. { unfold eq_key_elt, Raw.Proofs.PX.eqke in H2. apply X.lt_not_eq in H6. tauto. } { change ctn_raw2 with {| this := ctn_raw2; is_bst := H5 |}.(this) in H2. rewrite RangeTreeBag_btraverse_right_correct in H2; destruct H2. apply Raw.Proofs.MapsTo_In in H0; specialize (H7 _ H0). apply Raw.Proofs.L.PX.MO.lt_le in H6; eauto. } + exact IHctn_raw1. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts