Buenas tardes, estamos bastante trancados con la demostracion de este Lemma:
Lemma L10_6: forall m n: nat, prod m n = O -> m = O \/ n = O.
podrian guiarnos un poco?, pudimos utilizando allNat hacer como una primera demostacion, pero luego como que volvimos a tener que probar lo mismo y no pudimos probarlo.
Gracias, Saludos!
Hola Agustina
Está bien usar allNat en el segundo argumento del producto, ya que hay dos axiomas que estabecen el comportamiento del producto sobre dicho argumento.
El caso para cero es simple, ya que corresponde a right en el or.
Para el otro caso, notar que el caso que se demuestra del or es el izquierdo. Deberías elminar el existe que se genera para sacar información de ahí. Notar que al hacer ciertas reescrituras (incluyendo prodS), podrías usar el lema anterior (10.7) para concluir la prueba.
Espero que esto ayude, sino volvé a escribir.
Saludos, Carlos