Theorem: Nat.sub_le_right (GMLInit/Data/Nat/Sub.lean)

State before:
x y : Nat
⊢ x - y ≤ x
Tactic:
rw [Nat.sub_le_iff_le_add]
State after:
x y : Nat
⊢ x ≤ x + y

State before:
x y : Nat
⊢ x ≤ x + y
Tactic:
exact Nat.le_add_right ..
State after:
no goals