How to show injectivity of a function?

Here's what I'm trying to prove: Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

The + is notation for plus, defined as in https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O ⇒ m
    | S n' ⇒ S (plus n' m)
  end.

In Agda, one can do cong (n + _) to use the fact that n + m = n + p for any n m p.

Coq's built-in tactices injection and congruence both seemed promising, but they only work for constructors.

I tried the following strategy and kept hitting weird errors or getting stuck:

make an inductive type for bundling up a proof of (n + m = s): Sum (n m s)
use the congruence tactic in a lemma that shows Sum (n m s) = Sum (n p s)
use constructing Sums, destruct, and the lemma to show that n + m = n + p

Is there an easier way to prove this? I feel like there must be some built-in tactic I'm missing or some trickery with unfold.

UPDATE

Got it:

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
Proof.
  intros. induction n.
  - exact H.
  - apply IHn.  (* goal: n + m = n + p *)
    simpl in H. (* H: S (n + m) = S (n + p) *)
    congruence.
Qed.

Thanks @ejgallego

Solution

Injectivity of plus is not an "elementary" statement, given that the plus function could be arbitrary (and non-injective)

I'd say the standard proof does require induction on the left argument, indeed using this method the proof quickly follows.

You will need injection when you arrive to a goal of the form S (n + m) = S (n + p) to derive the inner equality.