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

chore(library/init/nat): fix style

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-08 16:31:42 -07:00
parent 5043e30c8e
commit c6d44d2e49
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/nat.lean
View file

@ -173,10 +173,10 @@ namespace nat
le_of_succ_le H
theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
le.rec (nat.le_refl (succ n)) (λa b, le.step)
le.rec (nat.le_refl (succ n)) (λ a b, le.step)
theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
le.rec (nat.le_refl (pred n)) (nat.rec (λa b, b) (λa b c, le.step))
le.rec (nat.le_refl (pred n)) (nat.rec (λ a b, b) (λ a b c, le.step))
theorem le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m :=
pred_le_pred