is mentioned by

Thm* x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi

[mod_minus]

In prior sections: bool 1 sqequal 1 prog 1 mb nat int 2 mb basic num thy 1

Try larger context: Graphs