α : Type ?u.131620
β : Type ?u.131623
γ : Type ?u.131626
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
⊢ 0 - a ≤ 0
α : Type ?u.131620
β : Type ?u.131623
γ : Type ?u.131626
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
⊢ 0 - a = 0
rw [← Ordinal.le_zero]
no goals
α : Type ?u.131620
β : Type ?u.131623
γ : Type ?u.131626
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
⊢ 0 - a ≤ 0
apply sub_le_self