proposition: Lemma seq_eq_app start len l l' : seq start len = l ++ l' <-> length l <= len /\ seq start (length l) = l /\ seq (start + length l) (len - length l) = l'.
proof: Proof. revert start len; induction l; ins. repeat split; ins; desf; f_equal; lia. destruct len; ins. split; ins; desf; lia. specialize (IHl (S start) len); intuition; desf; intuition; auto using f_equal. rewrite Nat.add_succ_comm in *; ins. rewrite Nat.add_succ_comm in *; auto using f_equal, le_S_n. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation