no goals
α : Type ?u.77971
β : Type ?u.77974
γ : Type ?u.77977
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
n : ℕ
⊢ a + ↑n = b + ↑n ↔ a = b
simp only [le_antisymm_iff, add_le_add_iff_right]