theorem boolmod2 (n: nat): $ bool (n % 2) $;
2 != 0 -> n % 2 < 2
2 != 0 -> bool (n % 2)
2 != 0
bool (n % 2)