proposition: Proposition nataddreflectsleq { n m k : nat } : n + k <= m + k -> n <= m.
proof: Proof. destruct n. - intros ?; apply leq_0_n. - intro a. change (n.+1 + k) with (n + k).+1 in a. now apply (@nataddreflectslt n m k). Defined.
imports: Basics Spaces.Nat.Core