no goals
α : Type ?u.130352
β : Type ?u.130355
γ : Type ?u.130358
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : b ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a
rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]