N_le@{} (n m : N) : Type@{p} := { k : N & k + n = m }. Notation "n <= m" := (N_le n m). Local Instance ishprop_N_le@{} n m : IsHProp (n <= m). Proof. apply ishprop_sigma_disjoint. intros x y e1 e2. apply N_add_cancel_r with n. path_via m. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.