proposition: Fact pos_list_NoDup n : NoDup (pos_list n).
proof: Proof. induction n as [|n IH]; simpl; constructor. - now intros [? [? ?]]%in_map_iff. - apply (FinFun.Injective_map_NoDup (@pos_nxt_inj n) IH). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)