proposition: Lemma OT_prod_assoc1 r g r' g': worder r -> substrate r = domain g -> order_type_fam g -> worder r' -> substrate r' = domain g' -> worder_fam g' -> r = order_sum r' g' -> (forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) -> let order_prod_assoc_aux := fun l => OT_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in OT_prod r g = OT_prod r' (Lg (domain g') order_prod_assoc_aux).
proof: Proof. move=> wor sr alB wor' sr' alw oal alfs osa. rewrite /OT_prod. have oa': orsum_ax r' g'. by split;fprops; move => t ta; move: (proj1 (alw _ ta)). apply: order_type_unique. set g'' := (Lg (domain g) (fun z => order_type_of (Vg g z))). have oa: orprod_ax r g''. rewrite /g'';red; aw;split => //; hnf;aw; move=> i idg; rewrite LgV//. apply: (OT_prop3 (OT_prop2 (alB _ idg))). move: (orprod_assoc_iso oa oa' oal wor' alw) => /=. set aux' := fun 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') aux'))); first by exists f. apply: orprod_invariant2 =>//; aww. rewrite sr';move=> i isr; rewrite LgV//; rewrite /osa /OT_prod;aw. rewrite ! LgV //; aw. set s:= order_prod _ _. have -> : (aux' i = s). rewrite /aux' /s; apply: 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''; aw; rewrite ! LgV//. have os: order s. rewrite /s; apply: orprod_or; saw; first fprops. hnf; aw;move=> j js; rewrite !LgV//. have jdg: inc (J j i) (domain g). rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. apply: (OT_prop3 (OT_prop2 (alB _ jdg))). by rewrite OT_prop4 //; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)