Idris2Doc : Data.Fin.Order

Data.Fin.Order

Implementation  of ordering relations for `Fin`ite numbers
data FinLTE : Fin k -> Fin k -> Type
Totality: total
Constructor: 
FromNatPrf : LTE (finToNat m) (finToNat n) -> FinLTE m n