Module t0 

Try to prove a goal given only a non-negative variable list.

Functions

prove

Try to prove a goal given only a non-negative variable list.

prove_shifted

prove given a constant lower bound per variable rather than a non-negative set. A variable with v >= c is rewritten as c + v' for a non-negative v', so 2*n - 2 >= 0 follows from n >= 1; a bound of 0 is the plain non-negative case.