proposition: Lemma comparable_ltgtP x y : x >=< y -> compare x y (min y x) (min x y) (max y x) (max x y) (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
proof: Proof. rewrite /min /max />=<%O !le_eqVlt [y == x]eq_sym. have := (eqVneq x y, (boolP (x < y), boolP (y < x))). move=> [[->//|neq_xy /=] [[] xy [] //=]] ; do ?by rewrite ?ltxx; constructor. by rewrite ltxx in xy. by rewrite le_gtF // ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)