michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat({library,hott}/init/nat): add sub_le_succ

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-15 21:38:41 +10:00
parent 3b010b8c92
commit 6b36076ab5
2 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
hott/init/nat.hlean
View file

@ -287,4 +287,5 @@ namespace nat
(le.refl a) (le.refl a)
(λ b₁ ih, le.trans !pred_le ih) (λ b₁ ih, le.trans !pred_le ih)
lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b)
end nat end nat

1
library/init/nat.lean
View file

@ -286,4 +286,5 @@ namespace nat
(le.refl a) (le.refl a)
(λ b₁ ih, le.trans !pred_le ih) (λ b₁ ih, le.trans !pred_le ih)
lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b)
end nat end nat