proposition: Fact lt_def x y : lt x y = (y != x) && le x y.
proof: Proof. rewrite /lt /le; case: x y => [x x'] [y y']//=; rewrite andbCA. case: (comparableP x y) => //= xy; last first. by case: _ / xy in y' *; rewrite !tagged_asE eq_Tagged/= lt_def. by rewrite andbT; symmetry; apply: contraTneq xy => -[yx _]; rewrite yx ltxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)