How to generate a Decidable inequality proof in Idris2?

Question

I know that Decidable.Equality has decDeq to be used for generating proofs about equality. For example, from this SO question, one can use decEq to decide if the length of a List is equal to the length of a target Vect, and then convert the List to Vect if the lengths are equal (code copied below).

I am trying to extend this and generate inequality proof. Given a List, I wanted to take the first n elements, provided that its number of elements is greater than or equal to n.

The original code with decEq is:

import Decidable.Equality
total
fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListOfLength n xs with (decEq (length xs) n)
  fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
  fromListOfLength n xs | (No _) = Nothing

I tried (unsuccessfully) to adapt this to inequalities as follows:

import Decidable.Decidable
total
fromListLenGE : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListLenGE n xs with (decide LTE (length xs) n)
  fromListLenGE n xs | (Yes prf) = ?xxx
  fromListLenGE n xs | (No _) = Nothing

I couldn't figure out how to use the decide method to generate the inequality proof. This is for learning purposes.

Could someone help explain how to generate the LTE proof here so as to take the first n elements?