case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ 0 < a * a → a ≠ 0

case mpr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ a ≠ 0 → 0 < a * a
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ 0 < a * a ↔ a ≠ 0
constructor
case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0 * 0
⊢ False
case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ 0 < a * a → a ≠ 0
rintro h rfl
case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0
⊢ False
case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0 * 0
⊢ False
rw [mul_zero] at h
no goals
case mp
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0
⊢ False
exact h.false
case mpr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a ≠ 0
⊢ 0 < a * a
case mpr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ a ≠ 0 → 0 < a * a
intro h
case mpr.inl
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

case mpr.inr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a
case mpr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a ≠ 0
⊢ 0 < a * a
cases' h.lt_or_lt with h h
no goals
case mpr.inl
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

case mpr.inr
α : Type u
β : Type ?u.211359
inst✝ : LinearOrderedRing α
a✝ b c a : α
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a
exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]