theorem proved tactic proof

`phi_sq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 202theorem phi_sq : phi ^ 2 = phi + 1 := by

proof body

Tactic-mode proof.

 203  unfold phi
 204  have h5 : (0 : ℝ) ≤ 5 := by norm_num
 205  have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
 206  nlinarith [hsq]
 207
 208/-- phi > 0 -/