[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
⊢ False
[PROOFSTEP]
have := mul_left_not_lt a h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
this : ¬EuclideanDomain.r (a * (b - a * b / a)) a
⊢ False
[PROOFSTEP]
rw [mul_sub, sub_eq_iff_eq_add'.2 (div_add_mod (a * b) a).symm] at this 
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
this : ¬EuclideanDomain.r (a * b % a) a
⊢ False
[PROOFSTEP]
exact this (mod_lt _ a0)
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ a * b / b = a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ b * a / b = a
[PROOFSTEP]
exact mul_div_cancel_left a b0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ a
[PROOFSTEP]
rw [← div_add_mod a b, h, add_zero]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0
[PROOFSTEP]
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
haveI := Classical.dec
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
simp only [b0, zero_mul]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
rw [mul_div_cancel_left _ b0]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a % b ↔ c ∣ a
[PROOFSTEP]
rw [← dvd_add_right (h.mul_right _), div_add_mod]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0
[PROOFSTEP]
simpa only [zero_mul] using mul_div_cancel 0 a0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1
[PROOFSTEP]
simpa only [one_mul] using mul_div_cancel 1 a0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b
[PROOFSTEP]
rw [← h, mul_div_cancel _ hb]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = c / a
[PROOFSTEP]
rw [← h, mul_div_cancel_left _ ha]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
by_cases hz : z = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
subst hz
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ x * y / 0 = x * (y / 0)
[PROOFSTEP]
rw [div_zero, div_zero, mul_zero]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
rcases h with ⟨p, rfl⟩
[GOAL]
case neg.intro
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * (z * p / z)
[PROOFSTEP]
rw [mul_div_cancel_left _ hz, mul_left_comm, mul_div_cancel_left _ hz]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a
[PROOFSTEP]
rw [← mul_div_assoc _ hab, mul_div_cancel_left _ hb]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
⊢ p / q ∣ p
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p
[PROOFSTEP]
rw [hq, zero_dvd_iff] at hpq 
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p
[PROOFSTEP]
rw [hpq]
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p
[PROOFSTEP]
use q
[GOAL]
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q
[PROOFSTEP]
rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, EuclideanDomain.mul_div_cancel _ hq]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0
[PROOFSTEP]
simp only [div_zero, dvd_zero]
[GOAL]
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
[PROOFSTEP]
rcases h with ⟨d, rfl⟩
[GOAL]
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
[PROOFSTEP]
refine' ⟨d, _⟩
[GOAL]
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel_left _ ha]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd a 0 = a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : a = 0 then 0
    else
      let_fun x := (_ : EuclideanDomain.r (0 % a) a);
      gcd (0 % a) a) =
    a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ 0 = a
[PROOFSTEP]
simp only [h, zero_mod, gcd_zero_left]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : ¬a = 0
⊢ (let_fun x := (_ : EuclideanDomain.r (0 % a) a);
    gcd (0 % a) a) =
    a
[PROOFSTEP]
simp only [h, zero_mod, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := (_ : EuclideanDomain.r (b % a) a);
      gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := (_ : EuclideanDomain.r (b % a) a);
      gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a = 0
⊢ b = gcd (b % a) a
[PROOFSTEP]
simp only [h, mod_zero, gcd_zero_right]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : ¬a = 0
⊢ (let_fun x := (_ : EuclideanDomain.r (b % a) a);
    gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b
[PROOFSTEP]
rw [gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b
[PROOFSTEP]
exact ⟨dvd_zero _, dvd_rfl⟩
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
[PROOFSTEP]
rw [gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
[PROOFSTEP]
exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0
[PROOFSTEP]
simpa [h] using gcd_dvd a b
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0
[PROOFSTEP]
exact gcd_zero_right _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b c x✝¹ : R
x✝ : c ∣ 0
H : c ∣ x✝¹
⊢ c ∣ gcd 0 x✝¹
[PROOFSTEP]
simpa only [gcd_zero_left] using H
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b
[PROOFSTEP]
rw [gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a
[PROOFSTEP]
exact IH ((dvd_mod_iff ca).2 cb) ca
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ a ∣ b
[PROOFSTEP]
rw [← h]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b
[PROOFSTEP]
apply gcd_dvd_right
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a
[PROOFSTEP]
rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').fst = gcd 0 x
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).fst = gcd 0 x✝
[PROOFSTEP]
rw [xgcd_zero_left, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').fst = gcd x y
[PROOFSTEP]
simp only [xgcdAux_rec h, if_neg h, IH]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
[PROOFSTEP]
rw [← gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
[PROOFSTEP]
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1, Prod.mk.eta]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : EuclideanDomain.P a b (r, s, t)
p' : EuclideanDomain.P a b (r', s', t')
⊢ EuclideanDomain.P a b (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using GCD.induction generalizing s t s' t' with
| H0 n => simpa only [xgcd_zero_left]
| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : EuclideanDomain.P a b (r, s, t)
p' : EuclideanDomain.P a b (r', s', t')
⊢ EuclideanDomain.P a b (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using GCD.induction generalizing s t s' t' with
| H0 n => simpa only [xgcd_zero_left]
| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : EuclideanDomain.P a b (0, s, t)
p' : EuclideanDomain.P a b (n, s', t')
⊢ EuclideanDomain.P a b (xgcdAux 0 s t n s' t')
[PROOFSTEP]

| H0 n => simpa only [xgcd_zero_left]
[GOAL]
case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : EuclideanDomain.P a b (0, s, t)
p' : EuclideanDomain.P a b (n, s', t')
⊢ EuclideanDomain.P a b (xgcdAux 0 s t n s' t')
[PROOFSTEP]
simpa only [xgcd_zero_left]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux a✝ s t b✝ s' t')
[PROOFSTEP]

| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux a✝ s t b✝ s' t')
[PROOFSTEP]
rw [xgcdAux_rec h]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux (b✝ % a✝) (s' - b✝ / a✝ * s) (t' - b✝ / a✝ * t) a✝ s t)
[PROOFSTEP]
refine' IH _ p
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t)
[PROOFSTEP]
unfold P at p p' ⊢
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ match (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t) with
  | (r, s, t) => r = a * s + b * t
[PROOFSTEP]
dsimp
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)
[PROOFSTEP]
rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ← mul_assoc,
  ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b
[PROOFSTEP]
have :=
  @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
    (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (a, 1, 0)
[PROOFSTEP]
dsimp [P]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
[PROOFSTEP]
rw [mul_one, mul_zero, add_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (b, 0, 1)
[PROOFSTEP]
dsimp [P]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
[PROOFSTEP]
rw [mul_one, mul_zero, zero_add]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
[PROOFSTEP]
rwa [xgcdAux_val, xgcd_val] at this 
[GOAL]
R✝ : Type u
inst✝¹ : EuclideanDomain R✝
inst✝ : DecidableEq R✝
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
⊢ a = 0
[PROOFSTEP]
rw [← mul_div_cancel a h0.2, h, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ lcm x y
[PROOFSTEP]
rw [lcm, hxy, div_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * z * gcd x y = x * y
[PROOFSTEP]
rw [mul_right_comm, mul_assoc, ← hz]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ lcm x y
[PROOFSTEP]
rw [lcm, hxy, div_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y
[PROOFSTEP]
rw [← mul_assoc, mul_right_comm, ← hz]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm x y ∣ z
[PROOFSTEP]
rw [lcm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
by_cases hxy : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
rw [hxy, div_zero]
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ 0 ∣ z
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at hxy 
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z
[PROOFSTEP]
rwa [hxy.1] at hxz 
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
suffices x * y ∣ z * gcd x y by
  cases' this with p hp
  use p
  generalize gcd x y = g at hxy hs hp ⊢
  subst hs
  rw [mul_left_comm, mul_div_cancel_left _ hxy, ← mul_left_inj' hxy, hp]
  rw [← mul_assoc]
  simp only [mul_right_comm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
cases' this with p hp
[GOAL]
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
use p
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
⊢ z = x * y / gcd x y * p
[PROOFSTEP]
generalize gcd x y = g at hxy hs hp ⊢
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
r : R
hr : x = gcd x y * r
s p g : R
hxy : ¬g = 0
hs : y = g * s
hp : z * g = x * y * p
⊢ z = x * y / g * p
[PROOFSTEP]
subst hs
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = x * (g * s) / g * p
[PROOFSTEP]
rw [mul_left_comm, mul_div_cancel_left _ hxy, ← mul_left_inj' hxy, hp]
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * (g * s) * p = x * s * p * g
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * g * s * p = x * s * p * g
[PROOFSTEP]
simp only [mul_right_comm]
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * gcd x y
[PROOFSTEP]
rw [gcd_eq_gcd_ab, mul_add]
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
[PROOFSTEP]
apply dvd_add
[GOAL]
case neg.intro.intro.intro.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y)
[PROOFSTEP]
rw [mul_left_comm]
[GOAL]
case neg.intro.intro.intro.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ x * (z * gcdA x y)
[PROOFSTEP]
exact mul_dvd_mul_left _ (hyz.mul_right _)
[GOAL]
case neg.intro.intro.intro.h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)
[PROOFSTEP]
rw [mul_left_comm, mul_comm]
[GOAL]
case neg.intro.intro.intro.h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y * x ∣ y * (z * gcdB x y)
[PROOFSTEP]
exact mul_dvd_mul_left _ (hxz.mul_right _)
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm 0 x = 0
[PROOFSTEP]
rw [lcm, zero_mul, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm x 0 = 0
[PROOFSTEP]
rw [lcm, mul_zero, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0
[PROOFSTEP]
intro hxy
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : lcm x y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy 
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
apply Or.imp_right _ hxy
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ y / gcd x y = 0 → y = 0
[PROOFSTEP]
intro hy
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
⊢ y = 0
[PROOFSTEP]
by_cases hgxy : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy 
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0
[PROOFSTEP]
exact hgxy.2
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y = 0
[PROOFSTEP]
generalize gcd x y = g at hr hs hy hgxy ⊢
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
r s g : R
hr : x = g * r
hs : y = g * s
hy : y / g = 0
hgxy : ¬g = 0
⊢ y = 0
[PROOFSTEP]
subst hs
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : g * s / g = 0
⊢ g * s = 0
[PROOFSTEP]
rw [mul_div_cancel_left _ hgxy] at hy 
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * s = 0
[PROOFSTEP]
rw [hy, mul_zero]
[GOAL]
case mpr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ x = 0 ∨ y = 0 → lcm x y = 0
[PROOFSTEP]
rintro (hx | hy)
[GOAL]
case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0
[PROOFSTEP]
rw [hx, lcm_zero_left]
[GOAL]
case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0
[PROOFSTEP]
rw [hy, lcm_zero_right]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y
[PROOFSTEP]
rw [lcm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
by_cases h : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at h 
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y
[PROOFSTEP]
rw [h.1, zero_mul]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
generalize gcd x y = g at h hr ⊢
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y
[PROOFSTEP]
subst hr
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel_left _ h]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
by_cases hc : c = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
simp [hc]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
refine' eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha _)
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * (c * (a * b / (a * c))) = a * b
[PROOFSTEP]
rw [← mul_assoc, ← mul_div_assoc _ (mul_dvd_mul_left a hcb), mul_div_cancel_left _ (mul_ne_zero ha hc)]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc0)
[GOAL]
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd0)
[GOAL]
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
obtain ⟨k1, rfl⟩ := hac
[GOAL]
case inr.inr.intro
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)
[PROOFSTEP]
obtain ⟨k2, rfl⟩ := hbd
[GOAL]
case inr.inr.intro.intro
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
[PROOFSTEP]
rw [mul_div_cancel_left _ hc0, mul_div_cancel_left _ hd0, mul_mul_mul_comm, mul_div_cancel_left _ (mul_ne_zero hc0 hd0)]
