Function prove 

pub fn prove(
    cmp: Cmp,
    lhs: &Poly,
    rhs: &Poly,
    nonneg: &dyn Fn(Var) -> bool,
) -> bool

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