case pos
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ ↑abv (-a) = ↑abv a

case neg
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) = ↑abv a
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
⊢ ↑abv (-a) = ↑abv a
by_cases ha : a = 0
case neg
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬↑abv (-a) = -↑abv a
case neg
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) = ↑abv a
refine'
  (mul_self_eq_mul_self_iff.mp (by rw [← map_mul abv, neg_mul_neg, map_mul abv])).resolve_right _
no goals
case neg
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬↑abv (-a) = -↑abv a
exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'
no goals
case pos
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ ↑abv (-a) = ↑abv a
simp [ha]
no goals
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : OrderedCommRing S
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ↑abv (-a) * ↑abv (-a) = ↑abv a * ↑abv a
rw [← map_mul abv, neg_mul_neg, map_mul abv]