theorem proved term proof

`phi_pos`

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

formal statement (Lean)

  65theorem phi_pos : 0 < φ := by

Term-mode proof.

  66  unfold φ
  67  have h := sqrt5_pos
  68  linarith
  69
  70/-- φ > 1 -/

Lean names referenced from this declaration's body.