proposition: Lemma map_seq_shift A (f g : nat -> A) a b n (EQ: forall i (LTi : i < n), f (a + i) = g (b + i)) : map f (seq a n) = map g (seq b n).
proof: Proof. induction n; try done. rewrite !seqS, !map_app; ins; f_equal. apply IHn; ins; apply EQ; lia. f_equal; apply EQ; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation