proposition: Lemma orprod_wor r g: worder_on r (domain g) -> worder_fam g -> finite_set (substrate r) -> worder (order_prod r g).
proof: Proof. move=> [wor sr] alw fs. have lea:orprod_ax r g by split => // i ie; exact (proj1 (alw _ ie)). move h: (cardinal (substrate r)) => n. have nN: natp n by apply /NatP; rewrite - h. clear wor sr fs; move:n nN r g lea alw h. apply: Nat_induction. move=> r g lea alw cr. move:(orprod_osr lea) => [lo]. rewrite /prod_of_substrates /fam_of_substrates -(proj32 lea). rewrite (card_nonempty cr) setXb_0' => s1. exact:(worder_set1 (conj lo s1)). move=> n nN hrec r g lea alwo csr. have lo: (order (order_prod r g)) by fprops. have [[or _] sr alo] := lea. apply:(worder_prop_rev lo) => [x xsr [x0 x0x]]. move: xsr;rewrite orprod_sr // => xsr. case: (emptyset_dichot (substrate r)) => nesr. by case: (@succ_nz n); rewrite - csr nesr cardinal_set0. move: (worder_least (proj31 lea) nesr) => [i []]; rewrite {1} sr => isr ilsr. set Y := fun_image x (fun z => Vg z i). have sYs: (sub Y (substrate (Vg g i))). move=> t /funI_P [z zx ->]; apply: prod_of_substrates_p; fprops. have neY: (nonempty Y) by exists (Vg x0 i); apply /funI_P; ex_tac. move: (worder_prop (alwo _ isr) sYs neY) => [z zY zl]. move: (proj1 (alwo _ isr)) => or'. set X1 := Zo x (fun t => Vg t i = z). have p1: (forall a b, inc a x -> inc b x -> inc a X1 -> ~ inc b X1 -> glt (order_prod r g) a b). move=> a b ax bx aX1 bX1; split; last by dneg ab; rewrite -ab. apply orprod_gleP =>//; split;fprops. right; exists i; split => //; first by ue. have ib: z <> Vg b i by move=> eq2; move: bX1 => /Zo_P; apply;split => //. have vbY: (inc (Vg b i) Y) by apply /funI_P; ex_tac. move: aX1 => /Zo_P [_ ->]; split => //; apply: (zl _ vbY). move=> j rj. have jsr: (inc j (substrate r)) by order_tac. move: (ilsr _ jsr) => le2; order_tac. set I1 := (substrate r) -s1 i. set r1 := induced_order r I1. set g1 := restr g I1. have I1sr: (sub I1 (substrate r)) by apply: sub_setC. have hh: sub I1 (domain g) by ue. have dg1: domain g1 = I1 by rewrite /g1;aw; trivial; ue. have sdg1g: sub (domain g1) (domain g) by rewrite dg1; ue. have la1: orprod_ax r1 g1. split => //. + move: lea => [WO _ _]; apply: induced_wor => //. + by rewrite /r1 iorder_sr. + hnf; rewrite /g1 => j j1; move: (alo _ (sdg1g _ j1)) => og1. by rewrite LgV//; ue. have alw: allf g1 worder. move=>j jdg; rewrite /g1 restr_ev; [by apply: alwo;apply: sdg1g| ue]. have cs: cardinal (substrate r1) = n. rewrite - sr in isr. rewrite /r1 /I1 iorder_sr // - cpred_pr5 // csr cpred_pr1; fprops. set X2 := fun_image X1 (fun z => restr z I1). have X2s: sub X2 (substrate (order_prod r1 g1)). rewrite orprod_sr//; move=> t /funI_P [u uX1 ->]; apply /setXb_P. have ux: (inc u x) by move: uX1=> /Zo_S. move: (xsr _ ux) => /prod_of_substratesP [fgfu du iVV]. aw;rewrite /g1 Lgd; split;fprops; move => j jI1; rewrite !LgV// ? Lgd//. apply: iVV; ue. have neX2: (nonempty X2). apply: funI_setne; move: zY => /funI_P [z0 z0x pz0];exists z0. by apply /Zo_P. move:(worder_prop (hrec _ _ la1 alw cs) X2s neX2)=> [w /funI_P [v vX1 rv] wle]. have vx: inc v x by move: vX1 => /Zo_S. have sxs: sub x (substrate (order_prod r g)) by rewrite orprod_sr. ex_tac. move=> u ux1. case: (equal_or_not (Vg u i) z)=> Vu; last first. have nv: (~ inc u X1) by move /Zo_P => [_]. by move: (p1 _ _ vx ux1 vX1 nv)=> [le _]. have uX1: (inc u X1) by apply: Zo_i. have rX2: (inc (restr u I1) X2) by apply /funI_P; ex_tac. move: (wle _ rX2). move /(orprod_gle1P la1) => [wp rp]; set T:= Zo _ _ => op. apply /(orprod_gle1P lea); split;fprops. have aa:sub (Zo (domain g) (fun i0 => Vg v i0 <> Vg u i0)) (substrate r). by rewrite sr; apply: Zo_S. move=> j []; rewrite (iorder_sr or aa) => /Zo_P [jd nsv] aux. have jI1: inc j I1. by apply /setC1_P;split => //; [ ue | dneg ij; rewrite ij Vu; move:vX1 => /Zo_P []]. move/prod_of_substratesP: (xsr _ vx) => [fgv dv vp]. move /prod_of_substratesP: (xsr _ ux1) => [fgu du up]. have pa: sub I1 (domain u) by rewrite du -dg1. have pb: sub I1 (domain v) by rewrite dv -dg1. have jT: inc j T by apply: Zo_i; [ue | rewrite rv !LgV]. have lej: (least (induced_order r1 T) j). move: (iorder_osr or I1sr) => [or1' sr1']. have sT: sub T (substrate r1) by rewrite /r1 iorder_sr // -dg1;apply: Zo_S. hnf;rewrite iorder_sr //; split =>// x1 aux2. move: (aux2) => /Zo_P []; rewrite dg1 => xi; rewrite rv !LgV// => pc. apply /(iorder_gle0P _ jT aux2); apply /(iorder_gle0P _ jI1 xi). have aux3: (inc x1 (Zo (domain g) (fun i => Vg v i <> Vg u i))). apply: Zo_i => //; ue. exact: (iorder_gle1 (aux _ aux3)). by move: (op _ lej); rewrite rv /g1 !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)