error005.idr:13:1:When checking right hand side of two with expected type
        Fin 2

When checking argument prf to function Data.Fin.fromInteger:
        When using 2 as a literal for a Fin 2 
                2 is not strictly less than 2
error005.idr:16:1:When checking right hand side of hahaha with expected type
        Fin n

When checking argument prf to function Data.Fin.fromInteger:
        When using 0 as a literal for a Fin n 
                0 is not strictly less than n
error005.idr:22:1:When checking right hand side of notOk with expected type
        Fin (plus 2 n)

When checking argument prf to function Data.Fin.fromInteger:
        When using 2 as a literal for a Fin (S (S n)) 
                2 is not strictly less than S (S n)
error005.idr:23:24:When checking right hand side of b0rken with expected type
        Fin 3

When checking argument prf to function Data.Fin.fromInteger:
        When using n as a literal for a Fin 3 
                Could not show that n is less than 3 because n is a bound
                variable instead of a constant Integer
error005.idr:28:1:When checking right hand side of x with expected type
        Fin 4

When checking argument prf to function Data.Fin.fromInteger:
        When using 5 as a literal for a Fin 4 
                5 is not strictly less than 4