N_lt_iff_succ_le@{} (n m : N) : (n < m) <-> (succ n <= m). Proof. split; intros [k H]; exists k. - rewrite N_add_succ, <- N_add_succ_l. assumption. - rewrite N_add_succ_l, <- N_add_succ. assumption. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.