proposition: Lemma comparableP x y : incompare 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) (y >=< x) (x >=< y).
proof: Proof. rewrite ![y >=< _]comparable_sym; have [c_xy|i_xy] := boolP (x >=< y). by case: (comparable_ltgtP c_xy) => ?; constructor. by rewrite /min /max ?incomparable_eqF ?incomparable_leF; rewrite ?incomparable_ltF// 1?comparable_sym //; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)