proposition: Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
proof: Proof. unfold remove_dups_fast; destruct l as [|x1 [|x2 l]]. - apply NoDup_nil_2. - apply NoDup_singleton. - apply NoDup_elements. Qed.
imports: stdpp(zmap) stdpp(options)