(n m : nat) : n.+1 - m <= (n - m).+1. Proof. revert m. simple_induction n n IHn. - simple_induction m m IHm; exact _. - intro m; simple_induction m m IHm. + apply leq_refl. + apply IHn. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.