Hola Camilo.
Abajo copio una solución.
Respecto a tu comentario: "Le_S : forall n m : nat, LE n m -> LE n (S m)." no permite junto con Le_O definir correctamente la relación. Solo podrías construir: LE O ?.
Una opción posible sería:
Inductive LE : nat -> nat -> Prop :=
| Le_O : forall n : nat, LE n n
| Le_S : forall n m : nat, LE n m -> LE n (S m).
Una posible solución de la tranistiva de LE con tu definición:
Theorem ej5_1_5 : forall n m k:nat , LE n m -> LE m k -> LE n k.
Proof.
induction n; simpl; intros; auto.
constructor.
inversion_clear H in H0.
inversion_clear H0.
constructor.
apply (IHn m0); assumption.
Qed.
Saludos, Carlos