proposition: Lemma nodup_prefix_of_nat n : NoDup (prefix_of_nat n).
proof: Proof. destruct PO; induction n; ins. all: repeat first [apply conj | apply nodup_filterP | rewrite nodup_app | rewrite nodup_cons | apply nodup_prefixes ]; ins. all: red; ins; in_simp; desf; rewrite in_prefixes in *; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt