proposition: Lemma orprod_total4: total_order (order_prod r g) -> all_big_substrate g -> exists f1 f2, [/\ inc f1 (substrate (order_prod r g)), inc f2 (substrate (order_prod r g)) & forall i, inc i (domain g) -> glt (Vg g i) (Vg f1 i) (Vg f2 i)].
proof: Proof. move=> tor ns. move:(all_big_substrate_prop ns) => [f1 [f2 [f1s f2s cf12]]]. move/prod_of_substratesP: f1s => [_ _ f1s]. move/prod_of_substratesP: f2s => [_ _ f2s]. have alne:(allf g ne_substrate). by move=> i idg; move: (f1s _ idg)=> h; exists (Vg f1 i). move/(orprod_total3P alne): tor => ror. have f0p i: inc i (domain g) -> glt (Vg g i) (inf (Vg g i) (Vg f1 i) (Vg f2 i)) (sup (Vg g i) (Vg f1 i) (Vg f2 i)). move => idg. move:(ror _ idg) (f1s _ idg) (f2s _ idg) (cf12 _ idg) => [os tos] xsr ysr xy. case (tos _ _ xsr ysr) => h. rewrite inf_comparable1 // sup_comparable1 //. rewrite inf_C sup_C inf_comparable1 // sup_comparable1 //; split; fprops. exists (Lg (domain g) (fun i=> (inf (Vg g i) (Vg f1 i) (Vg f2 i)))). exists (Lg (domain g) (fun i=> (sup (Vg g i) (Vg f1 i) (Vg f2 i)))). move: (oa) => [wor sr alo]. rewrite orprod_sr; split => //. apply: prod_of_substrates_gi => i idg; move: (f0p _ idg) => h; order_tac. apply: prod_of_substrates_gi => i idg; move: (f0p _ idg) => h; order_tac. move => i idg; rewrite !LgV//; exact: (f0p _ idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)