proposition: Fact diamond_add {elt} : Diamond Equal (@add elt).
proof: Proof. intros k k' e e' a b b' Hk <- <-. now apply add_add_2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)