From fc82b46171de6f976f86a3c91d71ad3e2ace04c9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jul 2015 08:18:30 -0400
Subject: [PATCH] chore(library/data/nat/examples/fib): cleanup example

---
 library/data/nat/examples/fib.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/library/data/nat/examples/fib.lean b/library/data/nat/examples/fib.lean
index bb9e1da94..4ce91ef9b 100644
--- a/library/data/nat/examples/fib.lean
+++ b/library/data/nat/examples/fib.lean
@@ -34,19 +34,19 @@ lemma fib_fast_aux_lemma : ∀ n, (fib_fast_aux (succ n)).1 = (fib_fast_aux n).2
 | (succ (succ n)) :=
   begin
     rewrite [fib_fast_aux_succ_succ],
-    rewrite [-prod.eta (fib_fast_aux (succ (succ n)))],
+    rewrite [-prod.eta (fib_fast_aux _)],
   end
 
-theorem fib_eq_fib_fast : ∀ n, fib n = fib_fast n
+theorem fib_eq_fib_fast : ∀ n, fib_fast n = fib n
 | 0     := rfl
 | 1     := rfl
 | (n+2) :=
   begin
-    have feq  : fib n = fib_fast n,               from fib_eq_fib_fast n,
-    have f1eq : fib (succ n) = fib_fast (succ n), from fib_eq_fib_fast (succ n),
+    have feq  : fib_fast n = fib n,               from fib_eq_fib_fast n,
+    have f1eq : fib_fast (succ n) = fib (succ n), from fib_eq_fib_fast (succ n),
     unfold [fib, fib_fast, fib_fast_aux],
-    rewrite [-prod.eta (fib_fast_aux (succ n))], esimp,
-    fold fib_fast (succ n), rewrite -f1eq,
+    rewrite [-prod.eta (fib_fast_aux _)],
+    fold fib_fast (succ n), rewrite f1eq,
     rewrite fib_fast_aux_lemma,
-    fold fib_fast n, rewrite -feq,
+    fold fib_fast n, rewrite feq,
   end