(vb_sympy.py stopped by the verifier after ~15 min without output: sympy simplify of nested square roots too slow; superseded by vb_lemmas_numeric.py)
