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

fix(library/data/nat/order): fixes #786

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-09 20:47:41 -07:00
parent 00582934ec
commit 5ca37dace0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/nat/order.lean
View file

@ -298,7 +298,7 @@ assume Plt, lt.trans Plt (self_lt_succ j)
/- other forms of induction -/
protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : ∀n, (∀m, m < n → P m) → P n) : P n :=
nat.rec (λm, not.elim !not_lt_zero)
nat.rec (λm h, absurd h !not_lt_zero)
(λn' (IH : ∀ {m : ℕ}, m < n' → P m) m l,
or.by_cases (lt_or_eq_of_le (le_of_lt_succ l))
IH (λ e, eq.rec (H n' @IH) e⁻¹)) (succ n) n !lt_succ_self