proposition: Lemma olex_lex: worder r -> olex r g = order_prod r g.
proof: Proof. have pd: order_fam g by move: ax=> [_ _]. move => h. have pc:orprod_ax r g by move: ax => [pa pb pc]. move: olex_osr => [o1 sr1]. move: (orprod_osr pc) => [o2 sr2]. have ss: substrate (order_prod r g) = substrate (olex r g) by ue. apply/order_exten =>// => x y. case: (equal_or_not x y) => exy. rewrite exy; split => pa; order_tac. rewrite ss; order_tac. rewrite - ss; order_tac. have sd: substrate r = domain g by move: ax => [_]. have wor: worder (olex_io r x y). apply: induced_wor => //; apply: Zo_S. split. move /(olex_gleP) => [xp yp aux]; apply /(orprod_gle1P pc);split => //. set io := induced_order _ _. have ->: io = (olex_io r x y) by rewrite /io - sd. case: aux; first by contradiction. move:(olex_nsve1 xp yp exy wor) => lp. move: wor => [or _ ] [_ h1] j pb; by rewrite -(unique_least or lp pb). move /(orprod_gle1P pc) => [xp yp pe]; apply (olex_gleP); split => //. move:(olex_nsve1 xp yp exy wor) => lp. right; split => //; apply: pe; rewrite - sd //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)