theorem proved term proof

`phi_psi_diff`

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

formal statement (Lean)

 105theorem phi_psi_diff : φ - ψ = Real.sqrt 5 := by

Term-mode proof.

 106  unfold φ ψ; ring
 107
 108/-- **THEOREM: φ⁻¹ = φ − 1** -/