R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
x✝ : R
a : R := x✝
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
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
x✝ : R
a : R := x✝
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 x✝ b
change P a b
no goals
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
x✝ : R
a : R := x✝
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
exact a0.symm ▸ H0 b