proposition: Lemma eq_comparison_axiom : Equality.axiom eq_comparison.
proof: Proof. move => a b. apply: (iffP idP). by case : a b => [] []. by move => ->; case :b . Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)