proposition: Lemma ler_antisym : forall (x y : G), x <<= y -> y <<= x -> x = y .
proof: Proof. Proof . case: ltr_sorderb => h3 h4 x y; rewrite !ler_ltreq. case/orP=> hxy; last by move/eqP: hxy. case/orP=> hyx; last by move/eqP: hyx. by move: (h4 _ _ _ hxy hyx); rewrite (h3 x). Qed . Lemma ler_trans : transitive (@lebDef G) . Proof . case: ltr_sorderb=> h1 h2. move=> x y z; rewrite !ler_ltreq; case/orP; last first. move/eqP->; case/orP; by [move-> | move/eqP->; rewrite eqxx orbT]. move=> hyx; case/orP; last by move/eqP<-; rewrite hyx. by move=> hxz; rewrite (h2 _ _ _ hyx). Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)