Consultas de Práctico

Hola,

¿Se puede usar la librería ZArith? En particular, ¿se puede usar la táctica 'omega'? La necesito para la parte 4 del ejercicio 18 del práctico 4.

Durante la demostración que se pide en ese ejercicio (probar que la cantidad de nodos externos es igual a la de los internos más uno), en determinado momento tengo en el goal una igualdad que se demuestra manipulando los términos (sumandos) de la igualdad. Planteo la igualdad en general como un lema (en el ejercicio, n y m representan la cantidad de nodos internos de sub árboles):

Require Import ZArith.

Lemma L : forall (n m:nat), n + 1 + (m + 1) = S (n + m + 1).
Proof.
  intros n m.
  rewrite plus_assoc_reverse.
  rewrite (Nat.add_comm 1 (m+1)).
  rewrite Nat.add_assoc.
  rewrite Nat.add_assoc.
  rewrite Nat.add_1_r.
  reflexivity.
Qed.

Después me di cuenta que se puede demostrar simplemente con la táctica 'omega' (también de ZArith).

Lemma L : forall (n m:nat), n + 1 + (m + 1) = S (n + m + 1).
Proof.
  intros.
  omega.
Qed.

Saludos,

Nicolás