no goals
α : Type ?u.132845
β : Type ?u.132848
γ : Type ?u.132851
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c d : Ordinal
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d
rw [sub_le, sub_le, sub_le, add_assoc]