ndcroos

Port Coq code to use 'done' tactic instead of 'easy' and benchmark

6

See https://github.com/coq-community/math-classes/issues/128 See also this discussion: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Error.20in.20MathClasses.2C.20adding.20an.20import Todo's: * benchmarking * hide fast_done

I agree to license my contributions to each file under the terms given at the top of each file I changed.