Partial quantifier elimination pQE finds hints on how to strengthen the assumptions in case
Tools → QE returns false or Tools → Counterexample indicates that the
assumptions are not strong enough.
See also
Tools → QE for quantifier elimination to decide the truth of formulas in real arithmetic.
Tools → Counterexample to get potentially faster feedback whether the sequent is suspected true or false.