proposition: Lemma orprod_total2: allf g ne_substrate -> ((total_order (order_prod r g) -> (allf g total_order)) /\ (worder (order_prod r g) -> (allf g worder))).
proof: Proof. move=> alne. move: (oa) => [wor sr pa]. pose f i t := Lg (domain g) (fun j => Yo (j = i) t (rep (substrate (Vg g j)))). have aux:forall i t, inc t (substrate (Vg g i)) -> inc (f i t) (substrate (order_prod r g)). move=> i t ts;rewrite orprod_sr //. rewrite /f; aw;apply /prod_of_substratesP;split => //; aww. by move => j jdg; rewrite LgV//; Ytac ji; [ ue | apply: rep_i; apply: alne]. have aux2: forall i t1 t2, inc i (domain g) -> inc t1 (substrate (Vg g i)) -> inc t2 (substrate (Vg g i)) -> gle (order_prod r g) (f i t1) (f i t2) -> gle (Vg g i) t1 t2. move=> i t1 t2 idg t1s t2s /(orprod_gleP oa) [_ _ h]. move: (pa _ idg) => oi; case: h. move=> eq; move: (f_equal (Vg^~ i) eq); rewrite /f !LgV//; Ytac0; Ytac0. by move=> ->; order_tac. rewrite sr; move=> [j [jsr j1 j2]]; move: j1; rewrite /f /glt; rewrite !LgV//. by Ytac ji; Ytac0; rewrite ? ji; case. split. move=> [or tor] i idg;move: (pa _ idg) => oi; split => //. move=> x y xsr ysr. by case: (tor _ _ (aux i _ xsr) (aux i _ ysr)) => h; [left | right ]; apply: aux2. move=> [or1 wor1]. move=> i idg; move: (pa _ idg) => oi; split => //. move=> x xsr xne. set (X:= fun_image x (f i)). have Xs: (sub X (substrate (order_prod r g))). by move=> t /funI_P [z zx ->];apply: aux; apply: xsr. have neX: (nonempty X) by apply:funI_setne. move: (wor1 _ Xs neX) => [y []]; rewrite iorder_sr// => yX yle. move: yX => /funI_P [z zx fz]; exists z;red; rewrite iorder_sr //;split => //. move=> t tx. have ft: (inc (f i t) X) by apply /funI_P; ex_tac. apply /iorder_gle0P => //. aw; move: (yle _ ft); rewrite fz => le3; move: (iorder_gle1 le3) => le4. by apply: aux2 => //; apply: xsr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)