proposition: Lemma imap_seq {A B} (l : list A) (g : nat → B) i : imap (λ j _, g (i + j)) l = g <$> seq i (length l).
proof: Proof. revert i. induction l as [|x l IH]; [done|]. csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal. apply imap_ext; simpl; auto with lia. Qed.
imports: stdpp(options)