Buenas,
Para el lema L10_5 podríamos usar el lema L10_4 para la prueba de m = 0 si tuviésemos la conmutatividad de la suma.
Si tuviésemos inducción tendríamos que la prueba de la conmutatividad sería separar en los cuatro casos 0 y sucesor de n y m, y por ejemplo la prueba con n = 0 y m = S m' podría ser:
0 + s m' = s (0 + m') =* s (m' + 0) = s m' = s m' + 0
donde marqué con un asterisco el paso inductivo.
En coq con la definición en particular que tenemos de nat no me estaría saliendo el paso inductivo. Tal vez nunca va a salir así? jeje. Alguna idea?