proposition: Lemma orprod_total r g: orprod_ax r g -> (allf g total_order) -> total_order (order_prod r g).
proof: Proof. move=> la alt. have [ol sl] := (orprod_osr la). have [[or wor] sr ao] := la. split=>//; rewrite sl; move=> x y xsr ysr. have fgf:fgraph (fam_of_substrates g) by rewrite/fam_of_substrates; fprops. set s:=(Zo (substrate r) (fun i => Vg x i <> Vg y i)). case: (emptyset_dichot s) => nse. suff xy: x = y by left; rewrite xy; order_tac; rewrite sl. apply: (setXb_exten xsr ysr). move=> i idg; ex_middle u;empty_tac1 i. by rewrite/s; apply: Zo_i; move: idg; rewrite/fam_of_substrates; aw; ue. have ssr: sub s (substrate r) by rewrite/s; apply: Zo_S. have [j jle] := (wor _ ssr nse). move: (jle)=> [];rewrite iorder_sr // => js jp. have jdg: inc j (domain g) by rewrite - sr; apply: ssr. have [orj torj] := (alt _ jdg). have px: (inc (Vg x j) (substrate (Vg g j))) by apply:prod_of_substrates_p. have py: (inc (Vg y j) (substrate (Vg g j))) by apply:prod_of_substrates_p. move:ysr; rewrite /prod_of_substrates/fam_of_substrates; aw. have [ois sir] :=(iorder_osr or ssr). move: js => /Zo_hi h h'. case: (torj _ _ px py) => leaux. left; apply /(orprod_gle1P la); rewrite - sr; split => // k kl. rewrite - (unique_least ois jle kl); split =>//. right; apply /(orprod_gle1P la); split => //. have <-: s=(Zo (domain g) (fun i => Vg y i <> Vg x i)). rewrite /s sr; set_extens t; move/Zo_P => [pa pb]; apply: Zo_i; fprops. move => k kl. by rewrite - (unique_least ois jle kl); split =>//; apply /nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)