proposition: Lemma olex_gleP x y: gle (olex r g) x y <-> olex_comp2_r r g x y.
proof: Proof. split; first by move /Zo_hi; aw. move =>h;apply Zo_i;last by aw. by move: h => [pa pb _]; apply : setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)