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
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
⊢ False
have := mul_left_not_lt a h
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
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
rw [mul_sub, sub_eq_iff_eq_add'.2 (div_add_mod (a * b) a).symm] at this
no goals
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
exact this (mod_lt _ a0)