no goals
α : Type ?u.162386
β : Type ?u.162389
γ : Type ?u.162392
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
⊢ a ≤ a + b
simpa only [add_zero] using add_le_add_left (Ordinal.zero_le b) a