Added Thomas' proposal for solving the long Speedith lemmata with SMT solvers in Isabelle.