proposition: Lemma comparable_ltNge x y : x >=< y -> (x < y) = ~~ (y <= x).
proof: Proof. move=> c_xy; apply/idP/idP => [/lt_geF/negP/negP//|]. by rewrite lt_neqAle eq_le; move: c_xy => /orP [] -> //; rewrite andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)