fact

out (res) { assert (res >= 0); }