no goals
α : Type ?u.54905
β : Type ?u.54908
γ : Type ?u.54911
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
⊢ a + b = a + c ↔ b = c
simp only [le_antisymm_iff, add_le_add_iff_left]