proposition: Lemma in_prefix_of_nat i j (LEQ: i <= j) (S : s (f i)) : In (f i) (prefix_of_nat j).
proof: Proof. apply prefix_of_nat_prefix in LEQ; desf. rewrite LEQ; apply in_or_app; left. destruct i; ins; rewrite filterP_app; ins; desf; rewrite ?in_app_iff in *; ins; desf; tauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt