From f74d7fc2664b4ef3ba2faa4ba3d149f403b3bb69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2015 16:56:05 -1000 Subject: [PATCH] refactor(library/data/real/basic): add extra step to help unifier --- library/data/real/basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 14a82a91ce..d161ee4934 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -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