proposition: Lemma olexp_gleh x y: (induced_order (opp_order r') (olex_nsv r' x y)) = olex_io (opp_order r') x y.
proof: Proof. have or': order r' by move: wor' => [ok _]. have pa: (olex_nsv (opp_order r') x y) = (olex_nsv r' x y). by rewrite /olex_nsv (proj2 (opp_osr or')). rewrite /olex_io pa //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)