let
mk_neglit a = mk_poslit (
Atom
.negate
Arith
.mk_neg a)