Strengthen `elemSmallerThanBound`
For a `n : Fin m`, we have `n < m`,
whereas `elemSmallerThanBound` only proves `n <= m`,
even though the name and the docstring suggest otherwise.
commit91039ee2e6b25608d5669e463367a8c79ce5c73f
authorJulian Kniephoff <me@juliankniephoff.com>
dateSat 1 Sep 2018, 22:12 (8 years ago)
parent8b1efd4
libs/contrib/Data/Fin/Extra.idr+2−2
@@ -4,6 +4,6 @@ import Data.Fin
44
55||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
66public export
7−elemSmallerThanBound : (n : Fin m) -> LTE (finToNat n) m
8−elemSmallerThanBound FZ = LTEZero
7+elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
8+elemSmallerThanBound FZ = LTESucc LTEZero
99elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)