no goals
α : Type ?u.246220
β : Type ?u.246223
γ : Type ?u.246226
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
a0 : a = 0
⊢ a * (b - c) = a * b - a * c
simp only [a0, zero_mul, sub_self]
no goals
α : Type ?u.246220
β : Type ?u.246223
γ : Type ?u.246226
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
a0 : ¬a = 0
d : Ordinal
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
rw [sub_le, ← le_div a0, sub_le, ← le_div a0, mul_add_div _ a0]