proposition: Lemma prefix_of_nat_prefix i j (LEQ : i <= j) : exists l, prefix_of_nat j = prefix_of_nat i ++ l.
proof: Proof. apply le_plus_minus in LEQ; rewrite LEQ; generalize (j - i) as n. clear; intro n; rewrite Nat.add_comm; induction n; ins; desf; eauto using app_nil_end. by rewrite IHn; eexists; rewrite <- app_assoc. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt