proposition: Lemma orprod_assoc_iso r g r' g': orprod_ax r g -> orsum_ax r' g' -> r = order_sum r' g' -> worder r' -> (forall i, inc i (domain g') -> worder(Vg g' i)) -> let order_sum_assoc_aux := fun l => order_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in let ordinal_prod_assoc := order_prod r' (Lg (domain g') order_sum_assoc_aux) in order_isomorphism (Lf (fun z => Lg (domain g') (fun l => Lg (substrate (Vg g' l)) (fun j => Vg z (J j l)))) (prod_of_substrates g) (substrate (ordinal_prod_assoc))) (order_prod r g) (ordinal_prod_assoc).
proof: Proof. move=> la oa oa_link wor' alwo F G. move: (oa) => [or' sr' alo']. move: (la) => [wor sr alo]. have dgpr: forall i j, inc i (domain g') -> inc j (substrate (Vg g' i)) -> inc (J j i) (domain g). move=> i j id jd; rewrite - sr oa_link; rewrite orsum_sr //. by apply: disjoint_union_pi1 =>//. have la1: forall i, inc i (domain g') -> orprod_ax (Vg g' i) (Lg (substrate (Vg g' i)) (fun i0 : Set => Vg g (J i0 i))). move=> i idg; split;aww. hnf; aw; move=> j js; rewrite LgV// ; apply: alo; apply: dgpr =>//. have la': orprod_ax r' (Lg (domain g') F). split => //;hnf;aw;trivial;move=> i idg'; rewrite /F LgV//; fprops. have oG: order G by rewrite /G; fprops. have s1: substrate (order_prod r g) = prod_of_substrates g by rewrite orprod_sr. have sG1: substrate G = productb (Lg (domain g') (fun i => substrate (F i))). rewrite /G orprod_sr // /prod_of_substrates /fam_of_substrates Lgd. by apply: f_equal; apply: Lg_exten; move=> i idg /=; rewrite LgV. have sG0: substrate G = (prod_of_substrates (Lg (domain g') F)). rewrite /G orprod_sr // /prod_of_substrates /fam_of_substrates Lgd. have sG2: substrate G = productb (Lg (domain g') (fun i => productb (Lg (substrate (Vg g' i))(fun i0 => substrate (Vg g (J i0 i)))))). rewrite sG1; f_equal; apply: Lg_exten. move=> i idg; rewrite /F orprod_sr //; last by apply: la1. congr productb; rewrite /fam_of_substrates; aw. by apply: Lg_exten; move=> x xs /=; rewrite LgV//. pose h z := Lg (domain g') (fun l => Lg (substrate (Vg g' l)) (fun j => Vg z (J j l))). have p1: forall z, inc z (prod_of_substrates g) -> inc (h z) (substrate G). move=> z zp; move: (zp) => /prod_of_substratesP [fgz dz iVV]. rewrite sG2; apply /setXf_P; rewrite /h;split;[fprops | by aw | ]. move=> i idg; rewrite LgV//; apply /setXf_P;split;aww. move => j js; rewrite LgV//; apply: iVV; exact (dgpr _ _ idg js). have p2: forall a b, inc a (prod_of_substrates g) -> inc b (prod_of_substrates g) -> h a = h b -> a = b. move=> a b /prod_of_substratesP [fga da iVVa] /prod_of_substratesP [fgb db iVVb] eqn. apply: fgraph_exten =>//; try ue; move=> x xda. move: xda; rewrite da - sr oa_link; rewrite orsum_sr // => xsr. move: (du_index_pr1 xsr) => [Qx Px px]. move: (f_equal (Vg ^~ (Q x)) eqn) => eq2. by move: (f_equal (Vg ^~ (P x)) eq2); rewrite /h !LgV//; rewrite px. have p3: forall x, inc x (substrate G) -> exists2 z, inc z (prod_of_substrates g) & x = (h z). move=> x;rewrite sG2 => /setXf_P [fgx dx iVVx]. exists (Lg (domain g) (fun w => Vg (Vg x (Q w)) (P w))). apply /prod_of_substratesP; split;aww; move=> i idg; rewrite LgV//. move : idg; rewrite - sr oa_link; rewrite orsum_sr // => xsr. move: (du_index_pr1 xsr) => [Qx Px px]; move: (iVVx _ Qx). move /setXf_P => [fg1 d1 ivv1]. by rewrite -{3} px; apply: ivv1. rewrite /h; symmetry;apply: fgraph_exten =>//;[ fprops | aw; ue | aw]. move=> j jdg /=; rewrite LgV//; move: (iVVx _ jdg) => /setXf_P [fgj dj iVV2]. apply: fgraph_exten; [ fprops | exact | aw; ue| aw]. by move=> w ws; rewrite !LgV//; aw; trivial; apply: dgpr. split;fprops; aw; first by saw => //;apply: lf_bijective. hnf; rewrite lf_source ; move=> a b ap bp; rewrite !LfV //. split. move /(orprod_gleP la) => [_ _ ha]; apply/(orprod_gleP la'). split; first by rewrite - sG0; apply: p1. by rewrite - sG0; apply: p1. case: ha; first by move=> ->; left. move=> [j [jsr [jlt diff] jle]]; right. move: jsr; rewrite oa_link; rewrite orsum_sr // => jsg'. move: (du_index_pr1 jsg') => [Qx Px px]. rewrite sr';ex_tac. have paux: forall c, inc c (prod_of_substrates g) -> inc (Vg (h c) (Q j)) (prod_of_substrates (Lg (substrate (Vg g' (Q j))) (fun i : Set => Vg g (J i (Q j))))). move=> i ic;move: (p1 _ ic); rewrite sG1. move /setXf_P=> [fgh dh ivv]; move: (ivv _ Qx); aw. rewrite /F orprod_sr //; apply: la1 => //. rewrite -/(h a) - /(h b) LgV//; rewrite /F ;split; last first. rewrite /h LgV//; dneg aa; move: (f_equal (Vg ^~(P j)) aa). by rewrite !LgV// px. apply/(orprod_gleP (la1 _ Qx));split => //; try apply: paux => //. right; ex_tac; rewrite LgV//. by rewrite /h !LgV // px. move=> i [ile ne]. have isr: inc i (substrate (Vg g' (Q j))) by order_tac. rewrite /h !LgV//; apply: jle; split; last by dneg aa; rewrite -aa; aw. rewrite oa_link; apply /orsum_gleP; split => //. apply: disjoint_union_pi1=> //. by right; aw. move=> i ilt. have idg: inc i (domain g') by rewrite - sr'; order_tac. rewrite /h !LgV//; apply: Lg_exten =>// k ks. apply: jle; split; last by move: ilt => [_ bad]; dneg aa; rewrite -aa; aw. rewrite oa_link; apply /orsum_gleP;split => //. - by apply: disjoint_union_pi1. - by hnf; aw; left. move/(orprod_gleP la') => [_ _ ha]; apply /(orprod_gleP la);split => //. case: ha; first by move=> eq; left; apply: p2. move=> [j [jsr jlt jle]]; right. rewrite sr' in jsr; move: jlt; rewrite /h /F !LgV//; move=> [le ns]. move: le; move /(orprod_gleP (la1 _ jsr)). move=> [p6 p7];case; first by move=> p8; case: ns. move=> [k [ks klt kle]]. rewrite sr; move: (dgpr _ _ jsr ks) => pd. ex_tac; first by move: klt; rewrite !LgV//. move=> i [lei nei]; move: lei;rewrite oa_link=> lti. have : inc i (substrate (order_sum r' g')) by order_tac. rewrite orsum_sr // => iso; move: (du_index_pr1 iso) => [Qdg Psg' pi]. move: (orsum_gle1 lti); aw; case => ch. move: (jle _ ch); rewrite /h !LgV// => eq1. by move: (f_equal (Vg ^~(P i)) eq1); rewrite !LgV//; rewrite pi. move: ch => [Qi aux]. have ->: i = J (P i) j by rewrite -Qi; aw. have aux2: glt (Vg g' j) (P i) k. by rewrite -Qi; split => //; dneg aa; rewrite -aa - Qi pi; aw. rewrite Qi in Psg'; move: (kle _ aux2); rewrite !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)