From 38557b5d6c25fcb9d5b1b3f5d1c2dcf3ed46f87f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Feb 2017 17:21:26 -0800 Subject: [PATCH] feat(library/init/data/nat/basic): missing lemma --- library/init/data/nat/basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index fb6d3dbec2..a36a150b4d 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -130,6 +130,10 @@ lemma pred_le : ∀ (n : ℕ), pred n ≤ n | 0 := less_than_or_equal.refl 0 | (succ a) := less_than_or_equal.step (less_than_or_equal.refl a) +lemma pred_lt : ∀ {n : ℕ}, n ≠ 0 → pred n < n +| 0 h := absurd rfl h +| (succ a) h := lt_succ_of_le (less_than_or_equal.refl _) + lemma sub_le (a b : ℕ) : a - b ≤ a := nat.rec_on b (nat.le_refl (a - 0)) (λ b₁, nat.le_trans (pred_le (a - b₁)))