# In Lean 4 how to use an implication in a hypothesis?

I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It should have an obvious proof (using only logic and equality), but I have not found relevant examples - a Cheatsheet does indicate "apply" or "specialize".

example (a b c x y : Peano) (h1: a = b → a + c = c + b) (h2: x = y) : x + c = c + y := by sorry

• I’m glad you found an answer. Please use backticks for code in the future. It makes it easier for everyone to read. Dec 28, 2023 at 19:25
• Also please include all relevant background definitions or imports. I guess in this particular case it doesn’t matter what Peano is, but that isn’t always clear. Also the way most people help is by copy and pasting your code into Lean, so it is important to provide a complete “minimal working example”. Dec 28, 2023 at 19:28
• Thanks for your suggestions. I will try to use MWE when appropriate. Jan 3 at 23:18

After realizing that h1 needs to be quantified, I found a proof:
example (x y z : Peano) (h1: ∀ a b c:Peano, a = b → a + c = c + b) (h2: x = y) : x + z = z + y := by