N_lt_succ_iff_le@{} (n m : N) : (n < succ m) <-> (n <= m). Proof. split; intros [k H]; exists k. - rewrite N_add_succ_l in H. exact (succ_inj _ _ H). - rewrite N_add_succ_l; apply ap, H. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.