ishprop_N_lt@{} n m : IsHProp (n < m). Proof. apply ishprop_sigma_disjoint. intros x y e1 e2. apply N_add_cancel_r with (succ n). rewrite !N_add_succ, <-!N_add_succ_l. path_via m. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.