proposition: Fact lt_def x y : lt x y = (y != x) && le x y.
proof: Proof. rewrite /lt /le; case: x y => [x1 x2] [y1 y2]//=; rewrite xpair_eqE. by case: (comparableP x1 y1); rewrite lt_def. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)