ineq_sub' (n k : nat) : k < n -> n - k = (n - k.+1).+1. Proof. intro ineq. destruct n. - contradiction (not_lt_zero_r k). - change (n.+1 - k.+1) with (n - k). apply leq_pred' in ineq. by apply nat_sub_succ_l. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.