Buenas tardes
Realizando el ejercicio 5.2 del práctico 4 me surgió la duda de si el problema se puede resolver con una sola recorrida del árbol. Lo resolví utilizando dos funciones auxiliares recursivas, una que calcula la cantidad de nodos externos y otra la cantidad de nodos internos. Se me ocurrió que se podría realizar una única función que sume 1 por cada nodo externo y reste 1 por cada nodo interno, pero no supe como trabajar con enteros en coq (es decir un tipo que incluya números negativos). La idea era que hicéramos esto?
Gracias y saludos