proposition: Lemma in_seq_iff a n l : In a (seq n l) <-> n <= a < n + l.
proof: Proof. revert n; induction l; ins; rewrite ?IHl; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation