@@ -127,6 +127,11 @@ using (k : Nat)
127127 instance Poset (Fin k) FinLTE where
128128 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
129129 finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
130+
131+ instance Decidable [Fin k, Fin k] FinLTE where
132+ decide m n with (decideNatLTE (finToNat m) (finToNat n))
133+ | Yes prf = Yes (FromNatPrf prf)
134+ | No disprf = No (\ (FromNatPrf prf) => disprf prf)
130135
131136 instance Ordered (Fin k) FinLTE where
132137 order m n =