title: How to show injectivity of a function?
body: <p>Here's what I'm trying to prove: <code>Theorem add_n_injective : forall n m p, n + m = n + p -&gt; m = p.</code></p>
  
  <p>The <code>+</code> is notation for <code>plus</code>, defined as in <a href="https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html" rel="nofollow noreferrer">https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html</a>:</p>
  
  <pre><code>Fixpoint plus (n : nat) (m : nat) : nat :=
    match n with
      | O ⇒ m
      | S n' ⇒ S (plus n' m)
    end.
  </code></pre>
  
  <p>In Agda, one can do <code>cong (n + _)</code> to use the fact that <code>n + m = n + p</code> for any n m p.</p>
  
  <p>Coq's built-in tactices <code>injection</code> and <code>congruence</code> both seemed promising, but they only work for constructors.</p>
  
  <p>I tried the following strategy and kept hitting weird errors or getting stuck:</p>
  
  <ul>
  <li><p>make an inductive type for bundling up a proof of (n + m = s): Sum (n m s)</p></li>
  <li><p>use the <code>congruence</code> tactic in a lemma that shows <code>Sum (n m s) = Sum (n p s)</code></p></li>
  <li><p>use constructing <code>Sum</code>s, <code>destruct</code>, and the lemma to show that n + m = n + p</p></li>
  </ul>
  
  <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 <code>unfold</code>.</p>
  
  <p><strong>UPDATE</strong></p>
  
  <p>Got it:</p>
  
  <pre><code>Theorem add_n_injective : forall n m p, n + m = n + p -&gt; 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.
  </code></pre>
  
  <p>Thanks @ejgallego</p>