proposition: Lemma ler_order : orderb (@lebDef G) .
proof: Proof. Proof . constructor. - exact: ler_refl. - move=> x y; case/andP; exact: ler_antisym. - exact: ler_trans. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)