(i j : nat) : i < nat_pred j -> i.+1 < j. Proof. intros ineq. assert (H := leq_succ ineq). assert (i < j) as X. { apply (@lt_lt_leq_trans _ (nat_pred j) _); [assumption | apply predn_leq_n]. } by rewrite <- (nat_succ_pred' j i). Defined.
Require Import Basics. Require Import Spaces.Nat.Core.