proposition: Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i).
proof: Proof. revert m i. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m i Hi; [lia| |lia]. rewrite seqZ_cons by lia. destruct i as [|i]; simpl. - f_equal; lia. - rewrite Z.pred_succ, IH by lia. f_equal; lia. Qed.
imports: stdpp(options)