proposition: Lemma ordprod_worder_bisP: all_big_substrate g -> ( ( allf g worder /\ finite_set (substrate r)) <-> worder (order_prod r g)).
proof: Proof. move=> ad; move: (oa) => [wor sr alo]; split. move=> [p1 p2]; apply: orprod_wor => //. move=> wop. move: (orprod_total4 (worder_total wop) ad) => [f1 [f2 [f1s f2s f12]]]. split. have p1: (allf g ne_substrate). move=> i idg; move: (f12 _ idg); exists (Vg f1 i); order_tac. by move: (orprod_total2 p1) => [_]; apply. set (f := fun i => Lg (domain g) (fun z => Yo (glt r z i) (Vg f1 z) (Vg f2 z))). have fs: (forall i, inc i (domain g) -> inc (f i) (substrate (order_prod r g))). move=> i idg; rewrite orprod_sr // /f; aw. apply: prod_of_substrates_gi. move=> j jdg; move: (f12 _ jdg) (alo _ jdg) => le2 o2. Ytac ca; order_tac. rewrite - sr in fs; apply: (worder_decreasing_finite wor wop fs). move=> i j ij. have isr: (inc i (substrate r)) by order_tac. have jsr: (inc j (substrate r)) by order_tac. have idg: (inc i (domain g)) by ue. have jdg: (inc j (domain g)) by ue. have aux: ~ glt r i i by case. have aux1: glt (Vg g i) (Vg (f j) i) (Vg (f i) i). by rewrite /f !LgV//; Ytac0; Ytac0; apply: f12. split; last first. by move: aux1 => [_ neq1]; dneg eq1; rewrite eq1. rewrite orprod_sr // in fs. apply /(orprod_gleP oa) ; split => //; try (apply: fs => //). right; exists i; split => //; move=> k ki. have kdg: (inc k (domain g)) by rewrite - sr; order_tac. have kj: glt r k j by move: wor => [or _];order_tac. by rewrite /f !LgV//; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)