[michocoq] Refactor maps and sets to make them more usable.

Refactor maps and sets to enable reasoning by induction. We represent maps by an underlying inductive type map_above_key k, where k is an option type. If m : map_above_key (Some a), then m is a non-empty map whose smallest key is a; if m : None, then m is an empty map. A map in Mi-Cho-Coq pairs up a key k and an underlying map m : map_above_key k.

We now have an inductive type comparison_proof that wraps a proof that compare a b = Lt (or Eq, Gt). This way we are able to destruct a term t : comparison_proof a b, and retain the original proof compare a b = Lt (or Eq, Gt), which allows us to carry out proofs of induction.

Replaces !158 (closed).