proposition: Lemma length_prefix_of_nat n (INJ : forall i j, i < j <= n -> f i <> f j) (SET : forall i, i <= n -> s (f i)) : n < length (prefix_of_nat n).
proof: Proof. assert (exists l, Permutation (prefix_of_nat n) (map f (List.seq 0 (S n)) ++ l)). 2: desc; rewrite H, length_app, length_map, length_seq; lia. generalize (prefix_of_nat n), (fun i => @in_prefix_of_nat i n). induction n; ins. by forward apply (H 0); ins; eauto; apply in_split_perm. forward apply (H (S n)); ins; eauto. forward apply IHn as X; intros; eauto. apply INJ; lia. desf. rewrite X, in_app_iff, in_map_iff in H0; desf. rewrite in_seq0_iff in *; eapply INJ in H0; try lia. apply in_split_perm in H0; desf. by exists l'; rewrite X, H0, <- (Nat.add_1_r (S n)), seq_add, map_app, <- app_assoc. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt