succ_seg@{} (n : N) : { m : N & m < n } -> { m : N & m <= n } := fun mh => let (m,H) := mh in (succ m; fst (N_lt_iff_succ_le m n) H).
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.