case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) y
obtain ⟨a, b, h⟩ := h
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y
use -a, b
no goals
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1
rwa [neg_mul_neg]