max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/data/nat/basic): missing lemma

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-07 17:21:26 -08:00
parent e06d6aa6d4
commit 38557b5d6c
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/nat/basic.lean
View file

@ -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₁)))