proposition: Lemma in_prefix_of_nat_in x n : In x (prefix_of_nat n) -> s x.
proof: Proof. induction n; ins; rewrite ?in_app_iff in *; in_simp. rewrite in_app_iff in *; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt