equal
deleted
inserted
replaced
297 then show ?case by simp |
297 then show ?case by simp |
298 next |
298 next |
299 case 2 |
299 case 2 |
300 then show ?case by (simp add: \<phi>_def real_le_lsqrt) |
300 then show ?case by (simp add: \<phi>_def real_le_lsqrt) |
301 next |
301 next |
302 case (3 n) term ?case |
302 case (3 n) |
303 have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n" |
303 have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n" |
304 by (simp add: field_simps power2_eq_square) |
304 by (simp add: field_simps power2_eq_square) |
305 also have "\<dots> = (\<phi> + 1) * \<phi> ^ n" |
305 also have "\<dots> = (\<phi> + 1) * \<phi> ^ n" |
306 by (simp_all add: \<phi>_def power2_eq_square field_simps) |
306 by (simp_all add: \<phi>_def power2_eq_square field_simps) |
307 also have "\<dots> = \<phi> ^ Suc n + \<phi> ^ n" |
307 also have "\<dots> = \<phi> ^ Suc n + \<phi> ^ n" |