proposition: Lemma ler_rcompat : rcompatible (@lebDef G).
proof: Proof. by move=> x y z; rewrite mulrC [z * _]mulrC; exact: ler_lcompat. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)