[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
R✝ : Type u
inst✝¹ : EuclideanDomain R✝
R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)
[PROOFSTEP]
rw [div_add_mod]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
[PROOFSTEP]
exact mul_left_not_lt b h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a
[PROOFSTEP]
simpa only [zero_mul, zero_add] using div_add_mod a 0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1
[PROOFSTEP]
simpa only [one_mul] using mul_left_not_lt 1 h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
b d : R
ha : b * d ≠ 0
⊢ d = 0 → b * d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
[PROOFSTEP]
exact mul_zero _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
a0 : a = 0
⊢ P a b
[PROOFSTEP]
change P a b
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
a0 : a = 0
⊢ P a b
[PROOFSTEP]
exact a0.symm ▸ H0 b
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      let_fun x := (_ : a % 0 ≺ 0);
      gcd (a % 0) 0) =
    a
[PROOFSTEP]
exact if_pos rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')
[PROOFSTEP]
unfold xgcdAux
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : 0 = 0 then (r', s', t')
    else
      let q := r' / 0;
      let_fun x := (_ : r' % 0 ≺ 0);
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')
[PROOFSTEP]
exact if_pos rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
conv =>
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
lhs
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t'
[PROOFSTEP]
rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      let q := r' / r;
      let_fun x := (_ : r' % r ≺ r);
      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
exact if_neg h
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdA 0 s = 0
[PROOFSTEP]
unfold gcdA
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1
[PROOFSTEP]
unfold gcdB
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]
