fact: Definition eq_comparison (a b:comparison) : bool := match a,b with | Lt,Lt => true | Eq,Eq => true | Gt,Gt => true | _,_ => false end.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)