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

chore: add Nat.le_refl as simp theorem

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-03 17:18:11 -08:00
parent 89c3820781
commit f629be745b
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Nat/Basic.lean
View file

@ -179,6 +179,8 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
/- Inequalities -/
attribute [simp] Nat.le_refl
theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
succ_le_succ