proposition: Lemma olex_osr: order_on (olex r g) (prod_of_substrates g).
proof: Proof. split => //; last by apply:olex_sr. move: (ax) => [[or tor] _ _]. have sd: substrate r = domain g by move: ax => [_]. apply: order_from_rel; split => //; last first. by move => x y [pa pb _];split; apply: olex_R. move=> x y => pa pb; ex_middle xny; symmetry. have pa': glt (olex r g) x y by split => //; apply /olex_gleP. move: pa pb => [pa pb pc] [_ _ pd]. case :pc => //; case: pd => //; rewrite /olex_comp1_r. move : (olex_glt_aux pa'); rewrite (olex_ioS r y x) /=. set i:=(the_least _). move => [isr _] [_ qb][_ qd]. suff h: order (Vg g i) by order_tac. by move: ax => [qe qf qh]; apply: qh; rewrite -qf. move => y x z pa pb. case: (equal_or_not x y) => exy; first by rewrite exy. case: (equal_or_not y z) => eyz; first by rewrite - eyz. have ltxy: glt (olex r g) x y by split => //; apply /olex_gleP. have ltyz: glt (olex r g) y z by split => //; apply /olex_gleP. move: pa pb => [xs ys xy] [_ zs yz]; split => //. case: (equal_or_not x z) => xz; first by left. right;case: xy => xy; first by contradiction. case: yz => yz; first by contradiction. move: (olex_glt_aux ltxy)(olex_glt_aux ltyz). move: xy yz; rewrite /olex_comp1_r /olex_io /olex_nsv. set Txy:= Zo _ _; set Tyz := Zo _ _; set Txz:= Zo _ _. set Ixy:=the_least _ . set Iyz:=the_least _ ; set Ixz:=the_least _. move => [woxy pxy][woyz pyz][ixys hixy][iyzs hiyz]. have sxz: sub Txz (Txy \cup Tyz). move => i /Zo_P [isr pa]; apply /setU2_P. case:(equal_or_not (Vg x i) (Vg y i)) => eq; [ right |left];apply: Zo_i =>//. ue. move: (ax) => [tor1 _]. have sxy: sub Txy (substrate r) by apply: Zo_S. have syz: sub Tyz (substrate r) by apply: Zo_S. have sxz1: sub Txz (substrate r) by apply: Zo_S. have p1: worder (induced_order r Txz) by apply: (union2_wor tor1 sxy syz sxz woxy woyz). have or1: order (Vg g Ixy) by move: ax => [_ _]; apply; ue. have or2: order (Vg g Iyz) by move: ax => [_ _]; apply; ue. split => //;case: (tor _ _ ixys iyzs) => cp. have lta: glt (Vg g Ixy) (Vg x Ixy) (Vg z Ixy). case: (equal_or_not Ixy Iyz) => eq2. move:pyz;rewrite -eq2; move => [aux _]; order_tac. have lt1: glt r Ixy Iyz by split. rewrite - (hiyz _ lt1)//. have it: inc Ixy Txz. apply: Zo_i; first by order_tac. move => neq; move: lta => [ _ aux]; contradiction. suff eq1: Ixz = Ixy by rewrite eq1. apply: the_least_pr2; first by move: p1 => [ok _]. red; rewrite iorder_sr //;split => //. move => j jt; apply /iorder_gleP => //. case: ( total_order_pr2 tor1 (sxz1 _ jt) ixys) => cp1 //. move: (hixy _ cp1) => eq1. have lt1: glt r j Iyz by order_tac. move: (hiyz _ lt1) => eq2. by move: jt =>/Zo_P; rewrite eq1 eq2;move => [_]. have lta: glt (Vg g Iyz) (Vg x Iyz) (Vg z Iyz). case: (equal_or_not Iyz Ixy) => eq2. move:pxy;rewrite -eq2; move => [aux _]; order_tac. have lt1: glt r Iyz Ixy by split. rewrite (hixy _ lt1)//. have it: inc Iyz Txz. apply: Zo_i => //. move => neq; move: lta => [ _ aux]; contradiction. suff eq1: Ixz = Iyz by rewrite eq1. apply: the_least_pr2; first by move: p1 => [ok _]. red; rewrite iorder_sr //;split => //. move => j jt; apply /iorder_gleP => //. case: ( total_order_pr2 tor1 (sxz1 _ jt) iyzs) => cp1 //. move: (hiyz _ cp1) => eq1. have lt1: glt r j Ixy by order_tac. move: (hixy _ lt1) => eq2. by move: jt => /Zo_P; rewrite eq2 eq1;move => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)