Buenas, logre terminar con todos los ejercicios menos el 10, estoy teniendo dificultades para demostrar la conmutatividad del producto, paso mi definición del producto:
Fixpoint prod (n m: nat): nat :=
match n with
| 0 => 0
| 1 => m
| S k => sum m (prod k m)
end.
Probé cambiar la definición haciendo match tanto en n como en m, pero de igual forma siempre me tranco en el paso inductivo de la demostración, hay algún lema auxiliar que me podría ayudar con esto o debería salir directamente?
Saludos, gracias.