no goals
α : Type ?u.162791
β : Type ?u.162794
γ : Type ?u.162797
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
⊢ a ≤ b + a
simpa only [zero_add] using add_le_add_right (Ordinal.zero_le b) a