Verify carbonated maps (3/3)

(this requires stdpp)

Verify the following lemmas in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/carbonated_map :

• add_key_values_to_map_is_valid
• of_list_is_valid
• merge_is_valid
• merge_eq
• fold_eq
• map_is_valid
• map_eq