no goals
α : Type ?u.135821
β : Type ?u.135824
γ : Type ?u.135827
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : ω ≤ o
⊢ 1 + o = o
rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, one_add_omega]