apply Nat.le_antisymm (Nat.sub_le_iff_left.mpr _)
                      (Nat.sub_le_iff_left.mpr $ Nat.sub_le_iff_left.mpr _)
a b c : Nat
⊢ a - (b + c) = a - b - c
a b c : Nat
⊢ a ≤ b + c + (a - b - c)

a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))