Forced one argument to be bigger than the other in Idris

Question

I'm trying to write a function mSmallestthat takes as input two integers n, and mcreates a vector. The output vector contains the msmallest members of a finite set with members n.

For example, mSmallest 5 3must create [FS (FS Z), FS Z, Z], which isVect 3 (Fin 5)

I would like to limit the input argument to mless than n. I tried something like this:

mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n > m = True} -> Vect m (Fin n)
mSmallest Z Z = ?c_3                                                                   
mSmallest Z (S k) = ?c_5                                                               
mSmallest (S k) m = ?c_2

The second case is not possible due to input p. How to do this to rule out the case Z (S k)?

Also, is there a better way to define a function mSmallest?

Answer 1

, n > m = True ; GT , , p:

-- Note that mSmallest is accepted as total with just this one case!
total mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n `GT` m} -> Vect m (Fin n)
mSmallest (S k) m {p = LTESucc p} = replicate m FZ

( mSmallest, ).