useless-casts-in-decreases-clauses.dfy(6,2): Info: decreases pos - 0

Dafny program verifier finished with 2 verified, 0 errors