Theorem: Nat.le_iff_exists_add' (Lean4Lean/Std/Basic.lean)

State before:
a b : Nat
⊢ a ≤ b ↔ ∃ c, b = c + a
Tactic:
simp [Nat.add_comm, Nat.le_iff_exists_add]
State after:
no goals