. rw [Nat.add_assoc]
  apply Nat.le_trans Nat.le_add_sub (Nat.add_le_add_left Nat.le_add_sub _)
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)))