proposition: Lemma olex_total2: total_order (olex r g) -> all_big_substrate g -> (worder r /\ (allf g total_order)).
proof: Proof. move=> pa pb. have pd: order_fam g by move: ax=> [_ _]. move: (proj2 olex_osr) => sr. move: (all_big_substrate_prop pb) =>[x [y [xsr ysr xney]]]. move/prod_of_substratesP: (xsr) => [_ _ aux]. move:(xsr)(ysr); rewrite - sr => xsr1 ysr1. have alne:(allf g ne_substrate). by move=> i idg; move: (aux _ idg)=> h; exists (Vg x i). have sd: substrate r = domain g by move: ax => [_]. have zp:olex_nsv r x y = domain g. rewrite /olex_nsv sd; set_extens w; first by move => /Zo_P []. by move => wg; apply: Zo_i => //; apply: xney. have or: order r by move: ax => [[or _] _]. case: (equal_or_not x y)=> exy. move: exy;rewrite (olex_nsve xsr ysr) zp => exy. split; last by move => t; rewrite exy; case; case. split => //; move=> X Xsr [z zX]; move: (Xsr _ zX) => au; empty_tac1 z; ue. have au: r = (olex_io r x y). rewrite /olex_io zp - sd iorder_substrate //. have wor: worder r. move: pa => [or1 tor]; case: (tor _ _ xsr1 ysr1) =>/olex_gleP. move=> [_ _ ]; case; [ done | move=> []; ue]. move=> [_ _];case; first by move => xy; case: exy. move => [h _]; by rewrite au olex_ioS. split =>//. move: pa; rewrite (olex_lex wor). have pc:orprod_ax r g by move: ax => [qa qb qc]. move: (orprod_total2 pc alne) => [pe _]; exact pe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)