proposition: Proposition nataddsub_comm_ineq_lemma (n m : nat) : n.+1 - m <= (n - m).+1.
proof: Proof. revert m. simple_induction n n IHn. - simple_induction m m IHm; [ apply leq_n | apply leq_S; apply leq_n ]. - intro m; simple_induction m m IHm. + apply leq_n. + apply IHn. Defined.
imports: Basics Spaces.Nat.Core