Buenos días, sé que el periodo de entrega del práctico culminó pero me quedé con la duda de como se resuelven estos dos ejercicios. Encontré este post que sugiere utilizar allNat, disc y sumS, entiendo el uso de los primeros dos pero no me queda claro como completar la demostración usando sumS
Gracias!
Hola.
Incluyo la prueba del primer lema para que veas aplicaciones de los axiomas referidos (en particular de sumS, según lo mencionás). La prueba del lema 10_5 te la dejo a vos (es un poco más larga).
Lemma L10_4: forall m n: nat, n <> O -> sum m n <> O.
Proof.
unfold not; intros m n H1 H2.
elim (allNat n); intro H3. (* notar que sum analiza casos para el segundo argumento: n *)
apply H1; assumption.
elim H3; intros x H4. (* en el caso del existe es necesario usar/obtener información de éste *)
rewrite <- H4 in H2.
rewrite sumS in H2. (* acá uso sumS *)
symmetry in H2. (* la igualdad está al revés para poder usar disc *)
apply (disc (sum m x)); assumption. (* y acá disc *)
Qed.
Saludos, Carlos
