Pappus' hexagon theorem and the ProveDetails command