no goals
α : Type ?u.249217
β : Type ?u.249220
γ : Type ?u.249223
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c b : Ordinal
x✝ : a ∣ a * b + c
d : Ordinal
e : a * b + c = a * d
⊢ c = a * (d - b)
rw [mul_sub, ← e, add_sub_cancel]
α : Type ?u.249217
β : Type ?u.249220
γ : Type ?u.249223
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c b : Ordinal
x✝ : a ∣ c
d : Ordinal
e : c = a * d
⊢ a ∣ a * (b + d)
α : Type ?u.249217
β : Type ?u.249220
γ : Type ?u.249223
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c b : Ordinal
x✝ : a ∣ c
d : Ordinal
e : c = a * d
⊢ a ∣ a * b + c
rw [e, ← mul_add]
no goals
α : Type ?u.249217
β : Type ?u.249220
γ : Type ?u.249223
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a c b : Ordinal
x✝ : a ∣ c
d : Ordinal
e : c = a * d
⊢ a ∣ a * (b + d)
apply dvd_mul_right