proposition: Lemma ltc_def x y : ltc x y = (y != x) && lec x y.
proof: Proof. move: x y => [a b] [c d] /=; simpc; rewrite eq_complex /=. by have [] := altP eqP; rewrite ?(andbF, andbT) //= lt_def. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)