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