(i j k : nat) : i < j -> k.+1 <= j -> k <= nat_pred j. Proof. intros l ineq. destruct j. - contradiction (not_lt_zero_r i). - by simpl; apply leq_pred'. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.