equiv_N_segment_lt_succ@{} (n : N) : { m : N & m < succ n } <~> {m : N & m <= n}. Proof. apply equiv_functor_sigma_id. intros; apply equiv_iff_hprop; apply N_lt_succ_iff_le. Defined.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.