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