proposition: Lemma osum_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' -> let order_sum_assoc_aux := fun l => osum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in osum r g = osum r' (Lg (domain g') (order_sum_assoc_aux)).
proof: Proof. move=> [wor sr] [wor' sr'] alB alw oal osa. have oa': orsum_ax r' g'. split;fprops; move => j jd; exact (proj1 (alw _ jd)). apply: ordinal_o_isu1. apply: orsum_wor; [saw| hnf; aw => i idg /=; rewrite LgcV; fprops]. apply: orsum_wor; [saw|hnf; aw=> i idg;rewrite !LgV//; aw; trivial ]. apply: ordinal_o_wor; rewrite /osa;apply: OS_sum=> //. by aw; split => //; apply:alw. hnf; aw => j js; rewrite LgV//;apply: alB;rewrite - sr oal (orsum_sr oa'). by apply: disjoint_union_pi1. set g'' := (Lgcomp g ordinal_o). have oa: orsum_ax r g''. rewrite /g'';hnf; saw;fprops; hnf; aw; move=> i idg. rewrite LgcV //; fprops. move: (orsum_assoc_iso oa oa' oal) => /=. pose aux' l:= order_sum (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_sum r' (Lg (domain g') aux'))); first by exists f. apply: orsum_invariant2 =>//;aww. rewrite sr' /Lgcomp;move=> i isr; rewrite !LgV// /osa /osum; aw; trivial. set s:= order_sum _ _. have -> : aux' i = s. rewrite /aux' /s/Lgcomp; aw; f_equal; apply: Lg_exten;move=> j js. have pd: inc (J j i) (domain g). rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. by rewrite /g'' LgcV// LgV//. apply: ordinal_o_is; apply: orsum_wor; first by split; [ apply: alw | aw]. hnf; aw;move=> j js; rewrite LgcV// ? Lgd // LgV//. 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)