Hola,
No se si me estoy complicando demasiado para probar la transitividad de la relación LE: forall n m p : nat, LE n m -> LE m p -> LE n p.
Hago inducción en p y utilizo dos lemas auxiliares:
Lemma le_n_S : forall n m : nat, LE n m -> LE n (S m).
Lemma n_le_m_or_eq : forall n m : nat, LE n (S m) -> LE n m \/ n = S m.
Con eso puedo demostrar la transitividad.
El problema es que no puedo demostrar el segundo lema (el primero sale por inducción en LE n m). Hago inducción en LE n (S m), pero me tanco en el caso inductivo:
2 subgoals
m, n, m0 : nat
H : LE n m0
IHLE : LE n m \/ n = m0
n_le_m : LE n m
______________________________________(1/2)
LE (S n) m \/ S n = S m0
______________________________________(2/2)
n = m0 -> LE (S n) m \/ S n = S m0
No veo qué me falta para terminar la demostración. Tal vez hay un camino más sencillo para demostrar la transitividad.
Saludos,
Nicolás