proposition: Lemma leC x y : (~` x <= ~` y) = (y <= x).
proof: Proof. gen have leC : x y / y <= x -> ~` x <= ~` y; last first. by apply/idP/idP=> /leC; rewrite ?complK. by move=> leyx; rewrite !complE leBr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)