aesop
case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
no goals