proposition: Lemma orprod_invariant3 r g: worder_on r (domain g) -> worder_fam g -> finite_set (substrate r) -> ordinal (order_prod r g) = oprod r (Lg (substrate r) (fun i => ordinal (Vg g i))).
proof: Proof. move => [wor sr] alo fsr. have or:= proj1 wor. apply: ordinal_o_isu1; first by apply: orprod_wor. apply: orprod_wor; aw => //. hnf; rewrite !Lgd; move=> i isr; rewrite !LgV // ? Lgd//. rewrite sr in isr; apply: (ordinal_o_wor (OS_ordinal (alo _ isr))). apply: orprod_invariant2 => //; first by aw. rewrite sr;move=> i isr; rewrite !LgV // ? Lgd //. apply: (ordinal_o_is (alo _ isr)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)