[michocoq] Add utility lemmas

Added a number of utility lemmas into base, tez, comparable. The util.v file is now obsolete and has been removed as the lemmas it contained are either not used or have been superseded.

In addition, we often need to supply the argument t explicitly in the proofs using eqb_eq and friends, and therefore we make it explicit.