α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ a * b = abs a * abs b ∨ a * b = -(abs a * abs b)
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ abs (a * b) = abs a * abs b
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
no goals
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c a b : α
⊢ a * b = abs a * abs b ∨ a * b = -(abs a * abs b)
cases' le_total a 0 with ha ha <;> cases' le_total b 0 with hb hb <;>
  simp only [abs_of_nonpos, abs_of_nonneg, true_or_iff, or_true_iff, eq_self_iff_true, neg_mul,
    mul_neg, neg_neg, *]