proposition: Lemma orprod_osr r g: orprod_ax r g -> order_on (order_prod r g) (prod_of_substrates g).
proof: Proof. move => ax; move: (ax)=> [wor sr ao]. have osr: substrate (order_prod r g) = prod_of_substrates g. rewrite /order_prod graph_on_sr //. move=> x _ j [js _]; move: js; rewrite iorder_sr //; fprops. by move /Zo_hi; case. by rewrite sr; apply: Zo_S. split => //. have tor: total_order r by apply: worder_total. split. + by apply: graph_on_graph. + by hnf; rewrite osr => y ya; apply/(orprod_gleP ax); split => //; left. + move => v u w ha. move/(orprod_gleP ax): (ha) => [ux _]; case; first by move ->. move => [j1 [j1sr hu1 hu2]]. move/(orprod_gleP ax) => [_ wx]; case;first by move <-. move => [j2 [j2sr hv1 hv2]]; apply/(orprod_gleP ax); split => //; right. case (equal_or_not j1 j2) => j12. exists j1; rewrite - j12 in hv1 hv2; split => //. rewrite sr in j1sr; exact:(lt_leq_trans (ao j1 j1sr) hu1 (proj1 hv1)). by move => i ha1; rewrite (hu2 _ ha1) (hv2 _ ha1). case:(proj2 tor _ _ j1sr j2sr) => h. exists j1; split => //; first by rewrite - (hv2 _ (conj h j12)). by move => i ia;rewrite (hu2 _ ia) (hv2 _ (lt_leq_trans (proj1 wor) ia h)). exists j2; split => //; first by rewrite (hu2 _ (conj h (nesym j12))). by move => i ia; rewrite - (hv2 _ ia) (hu2 _ (lt_leq_trans (proj1 wor) ia h)). move => u v. move/(orprod_gleP ax) => [_ _]; case => // [[j1 [j1sr hu1 hu2]]]. move/(orprod_gleP ax) => [_ _]; case => // [[j2 [j2sr hv1 hv2]]]. case: (equal_or_not j1 j2) => sj. move: hv1 => []; rewrite - sj => hv11; rewrite sr in j1sr. by rewrite(order_antisymmetry (ao j1 j1sr) (proj1 hu1) hv11). case:(proj2 tor _ _ j1sr j2sr) => h. by move: (hv2 _ (conj h sj)) (proj2 hu1) => ->. by move:(hu2 _ (conj h (nesym sj))) (proj2 hv1) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)