(i n k : nat) : (n > i) -> n <= k -> nat_pred n < k. Proof. intro ineq; destruct n. - contradiction (not_lt_zero_r i). - intro; assumption. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.