Lemmas for satisfiability modulo transcendental functions via incremental linearization