proposition: Lemma oprod_assoc1 r g r' g': worder_on r (domain g) -> worder_on r' (domain g') -> ordinal_fam g -> worder_fam g' -> r = order_sum r' g' -> finite_set (substrate r) ->finite_set (substrate r') -> (forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) -> let order_prod_assoc_aux := fun l => oprod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in oprod r g = oprod r' (Lg (domain g') order_prod_assoc_aux).
proof: Proof. move=> [wor sr] [wor' sr'] alB alw oal fs fs' alfs osa. have oa': orsum_ax r' g'. split;fprops; hnf; move => j jd; exact (proj1 (alw _ jd)). apply: ordinal_o_isu1. apply: orprod_wor; hnf; aw => //; move=> i idg; rewrite !LgV //; fprops. apply: orprod_wor; hnf; aw => // i idg'; rewrite !LgV//; aw; trivial. apply: ordinal_o_wor. rewrite /osa; apply:OS_prod; first by split; aww. hnf; aw;move => j js; rewrite LgV//; apply: alB. rewrite - sr oal (orsum_sr oa'). by apply: disjoint_union_pi1. by apply: alfs. set g'' := Lgcomp _ _. have oa: orprod_ax r g''. rewrite /g'';hnf; saw => //;hnf; aw; move=> i idg; rewrite !LgV//; fprops. move: (orprod_assoc_iso oa oa' oal wor' alw) => /=. pose ax' l := order_prod (Vg g' l) (Lg (substrate (Vg g' l))(fun i=> Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_prod r' (Lg (domain g') ax'))); first by exists f. apply: orprod_invariant2 =>//; aww. rewrite sr';move=> i isr;aw; rewrite /osa /oprod !LgV//; aw; trivial. set s:= order_prod _ _. have -> : (ax' i = s). rewrite /ax' /s /Lgcomp; aw; f_equal; apply: Lg_exten;move=> j js. have pd: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g'' ! LgV//. apply: ordinal_o_is;apply: orprod_wor; [ by split; aww | | fprops]. hnf; aw;move=> j js; rewrite !LgV //;aw;trivial; apply: ordinal_o_wor; apply: alB. rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)