fixed error withimplicit operation in prob + missing state existens check

f(s:set of nat)n:nat
post r in set s