proposition: Lemma Kcompare_trans : Trans K.compare.
proof: Proof. intros [ ] x y z; rewrite ?compare_eq_iff, ?compare_lt_iff, ?compare_gt_iff; order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)