proposition: Lemma olexp_gleP x y: gle olexp x y <-> [/\ inc x olexp_G, inc y olexp_G & ( x = y \/ (exists j, [/\ inc j (substrate r'), glt r (Vg x j) (Vg y j) & forall i, glt r' j i -> Vg x i = Vg y i]))].
proof: Proof. split. by move => /iorder_gleP [pa pb pc];split => //; apply /olexp_gle1P. by move => [pa pb pc]; apply /iorder_gleP;split => //;apply /olexp_gle1P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)