N_le_eq_or_lt@{} (n m : N) (H : n <= m) : (n = m) + (n < m). Proof. assert (HP : IsHProp ((n = m) + (n < m))). { apply ishprop_sum; try exact _. intros [] [l K]. apply N_add_cancel_zero_r in K. symmetry in K; apply zero_neq_succ in K; assumption. } destruct H as [k K]. destruct (N_zero_or_succ k) as [k0|[l L]]. - rewrite k0 in K. rewrite (N_add_zero_l n) in K. exact (inl K). - rewrite L in K. exact (inr (l;K)). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.