no goals
α : Type ?u.132338
β : Type ?u.132341
γ : Type ?u.132344
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a - b = 0
⊢ a ≤ b
simpa only [h, add_zero] using le_add_sub a b
no goals
α : Type ?u.132338
β : Type ?u.132341
γ : Type ?u.132344
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a ≤ b
⊢ a - b = 0
rwa [← Ordinal.le_zero, sub_le, add_zero]