Theorem plus_n_n_injective, exercise

Question

Help needed with an exercise from Software Foundations. This is the theorem:

Theorem plus_n_n_injective : ∀n m,
 n + n = m + m →
 n = m.
Proof.

I end up with n = 0 as goal and n + n = 0 as hypothesis. How to move on?

Answer 1

n + n cannot be simplified further because n is a variable, not a type constructor. You can expose all the construction cases of n by destructing it as Ptival said. However using inversion in this context seems to me a bit extreme and not what this Sf exercise is about.

When replaced by the O constructor, O + O will reduce (using simpl for example) to O and reflexivity should do the trick.

When replaced by the S constructor, S foo + bar will always reduce to the shape S something, which can't be equal to O (the easiest way to assert that is by using discriminate) because they are two constructors of the same type.

Best, V.