Estoy tratando de demostrar que, en mi opinión, es un teorema razonable:

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

La prueba por inducción llega al punto donde necesito probar esto:

lemma1 : (n : Nat) -> (n - 0) = n

Esto es lo que sucede cuando intento probarlo (el lema, por simplicidad) usando el probador interactivo:

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

Sentí que me faltaba algo sobre la definición de menos, así que lo busqué en la fuente:

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

¡La definición que necesito está ahí!minus left Z = left. Entiendo que Idris debería reemplazarminus m 0 conm aquí, y esto es entonces reflexivamente cierto. ¿Qué me he perdido?