Idris2Doc : Data.Fin.Order

Data.Fin.Order

Implementation  of ordering relations for `Fin`ite numbers
dataFinLTE : Fink -> Fink -> Type
Totality: total
Constructor: 
FromNatPrf : LTE (finToNatm) (finToNatn) -> FinLTEmn