@@ -4,6 +4,6 @@ import Data.Fin
5||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
5||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
6public export
6public export
7−elemSmallerThanBound : (n : Fin m) -> LTE (finToNat n) m
7+elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
8−elemSmallerThanBound FZ = LTEZero
8+elemSmallerThanBound FZ = LTESucc LTEZero
9elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
9elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)