error005.idr:13:1:When elaborating right hand side of two: When elaborating argument prf to function Data.Fin.fromInteger: When using 2 as a literal for a Fin 2 Could not show that 2 is less than 2 error005.idr:16:1:When elaborating right hand side of hahaha: When elaborating argument prf to function Data.Fin.fromInteger: When using 0 as a literal for a Fin n Could not show that 0 is less than n error005.idr:21:1:When elaborating right hand side of notOk: When elaborating argument prf to function Data.Fin.fromInteger: When using 2 as a literal for a Fin (S (S n)) Could not show that 2 is less than S (S n)