. intros h
  rw [Nat.add_comm]
  apply Nat.le_add_of_sub_le
  exact h
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c

case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c