proposition: Lemma olexp_Gxy1 x y: inc x olexp_G -> inc y olexp_G -> worder (olex_io (opp_order r') x y).
proof: Proof. move=> pa pb; move: (olexp_Gxy pa pb) => fs. have h:sub (olex_nsv (opp_order r') x y) (substrate (opp_order r')) by apply: Zo_S. apply: finite_set_torder_wor. apply: total_order_sub => //. by apply: total_order_opposite; apply worder_total. rewrite iorder_sr //. by move: wor' =>[or' _]; apply: (proj1 (opp_osr or')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)