Hola.
Respondí previamente sobre este lema. Acá inj no te sirve; estás confundiendo hipótesis con tesis (lo que tenés y lo que precisás probar).
Lemma L10_1: (sum (S O) (S O)) = (S (S O)).
Proof.
rewrite sumS.
rewrite sum0.
reflexivity.
Qed.
Saludos, Carlos