move the reduction control of the proofmode to its own file and tweak it See merge request FP/iris-coq!150