Here is a short proof:

Require Import Arith Lia.
Import EqNotations.

(* A generalised lemma, which generalises over the index using a
proof of equality to make case distinction well-defined. *)
Lemma le_n_eq_gen n m (e : m = n) (h : n <= m) : rew e in h = le_n n :> (n <= n).
Proof.
  destruct h.
  - (* to get rid of the n = n proof, we need UIP to replace it by reflexivity.
    I don't think this step can be avoided. *)
    rewrite (UIP_nat _ _ e eq_refl).
    reflexivity.
  - (* the other case is impossible by arithmetic reasoning, lia can take care of that. *)
    lia.
Qed.

(* now the corollary is trivial *)
Corollary le_n_eq n (h : n <= n) : h = le_n n.
Proof.
  apply (le_n_eq_gen eq_refl).
Qed.

Here we did not need any induction on the equality proof, only destruct. Had we needed it, the standard induction for le derived by Coq would not have been sufficient, because it is non-dependent, and so we cannot use it to prove properties of a proof witness. To derive the dependent induction principle, one can use:

Scheme Induction for le Sort Prop.
About le_ind_dep. (* the induction principle we really want to use. *)

Here is a short proof:

Require Import Arith Lia.
Import EqNotations.

(* A generalised lemma, which generalises over the index using a
proof of equality to make case distinction well-defined. *)
Lemma le_n_eq_gen n m (e : m = n) (h : n <= m) : rew e in h = le_n n :> (n <= n).
Proof.
  destruct h.
  - (* to get rid of the n = n proof, we need UIP to replace it by reflexivity.
    I don't think this step can be avoided (but note that the UIP we use is a 
    proven theorem from the standard library, not an axiom/assumption. *)
    rewrite (UIP_nat _ _ e eq_refl).
    reflexivity.
  - (* the other case is impossible by arithmetic reasoning, lia can take care of that. *)
    lia.
Qed.

(* now the corollary is trivial *)
Corollary le_n_eq n (h : n <= n) : h = le_n n.
Proof.
  apply (le_n_eq_gen eq_refl).
Qed.

Here we did not need any induction on the equality proof, only destruct. Had we needed it, the standard induction for le derived by Coq would not have been sufficient, because it is non-dependent, and so we cannot use it to prove properties of a proof witness. To derive the dependent induction principle, one can use:

Scheme Induction for le Sort Prop.
About le_ind_dep. (* the induction principle we really want to use. *)