proposition: Lemma ler_total : forall x y, (x <<= y) || (y <<= x) .
proof: Proof. Proof . by case G => [T [? []]] . Qed . Lemma ler_lcompat : lcompatible (@lebDef G) . Proof . move=> x y z; rewrite !ler_ltreq => px. case/orP; last by move/eqP->; rewrite eqxx orbT. move=> hyz; case/orP: px => hx; first by rewrite ltr_lcompat. by rewrite -(eqP hx) !mul0r eqxx orbT. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)