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

refactor(library/data/real/basic): add extra step to help unifier

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-31 16:56:05 -10:00
parent e01b155b2e
commit f74d7fc266
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/data/real/basic.lean
View file

@ -254,7 +254,8 @@ theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of
by rewrite [add.comm 1 (abs (s pone)), rat.add.comm 1, rat.add.assoc]
... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : rat.add_le_add_right (!ubound_ge)
... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add
... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc
... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc
... = rat_of_pnat (K s) : by esimp
theorem bdd_of_regular {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : ℕ+, s n ≤ b :=
begin