proposition: Lemma nodup_seq n l : NoDup (seq n l).
proof: Proof. revert n; induction l; ins; constructor; ins; eauto. rewrite in_seq_iff; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation