theorem
proved
term proof
Z_life_pos
show as:
view Lean formalization →
formal statement (Lean)
73theorem Z_life_pos : 0 < Z_life := by
proof body
Term-mode proof.
74 unfold Z_life
75 exact pow_pos phi_pos _
76