Theorem: LoVe.quarter_pos (LoVe/Homework/Homework9.lean)

State before:
x : ℚ
hx : 0 < x
⊢ 0 < x / 4
Tactic:
have hx2 : 0 < x / 2 := half_pos hx
State after:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ 0 < x / 4

State before:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ 0 < x / 4
Tactic:
calc 0 < (x / 2) / 2 := half_pos hx2
     _ = x / 4 := by ring
State after:
no goals

State before:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ x / 2 / 2 = x / 4
Tactic:
ring
State after:
no goals