proposition: Lemma orsum_assoc_iso r g r' g': orsum_ax r g -> orsum_ax r' g' -> r = order_sum r' g' -> let order_sum_assoc_aux := fun l => order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in let order_sum_assoc := order_sum r' (Lg (domain g') order_sum_assoc_aux) in order_isomorphism (Lf (fun x=> J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate (order_sum_assoc))) (order_sum r g) (order_sum_assoc).
proof: Proof. move=> oa oa' oa_link F G. move: (oa) => [or sr alo]. move: (oa') => [or' sr' alo']. have alo'' :forall l, inc l (substrate r') -> orsum_ax (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))). move=> l ls; saw; first by apply: alo' =>//; ue. hnf; aw;move => i isg; rewrite LgV //;apply: alo; rewrite - sr oa_link. rewrite orsum_sr //; apply: disjoint_union_pi1 =>// ; ue. have aux2 :forall l, inc l (domain g') -> order (F l). move=> l ldg'; rewrite /F; rewrite - sr' in ldg'; fprops. have oa'' : orsum_ax r' (Lg (domain g') F). hnf; saw; hnf; aw. by move => i idf; rewrite LgV//; apply: aux2. have org : order G by rewrite /G; fprops. have ta: (lf_axiom (fun x => J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate G)). move=> x xs; rewrite /G; aw; move: (du_index_pr1 xs) => [Qd Ps px]. move: Qd;rewrite - sr oa_link. rewrite !orsum_sr // => Qd. move: (du_index_pr1 Qd) => [QQd PQs pQ]. apply: disjoint_union_pi1; aw; trivial; rewrite LgV// /F orsum_sr //. by apply: disjoint_union_pi1;aw; trivial; rewrite LgV // pQ. apply: alo''; ue. set(FF:= Lf (fun x => J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate G)). have injF: injection FF. apply: lf_injective => //. move => u v us vs eq. move: (du_index_pr1 us) (du_index_pr1 vs) => [Qu _ <-][Qv _ <-]. move: (pr1_def eq) (pr2_def eq)=> eq1 eq2. move: Qu Qv;rewrite - sr oa_link; rewrite orsum_sr // => Qu Qv. move: (du_index_pr1 Qu)(du_index_pr1 Qv) => [_ _ <-][_ _ <-]. by rewrite eq2 (pr1_def eq1) (pr2_def eq1). have bF: (bijection FF). split =>//; apply: lf_surjective => //. move=> y; rewrite /G orsum_sr // => yG. move: (du_index_pr1 yG); rewrite Lgd=> [[Qd]]; rewrite LgV//; move=> Py Qpy. rewrite sr' in alo''; move: (alo'' _ Qd) => al. move: (Py); rewrite /F orsum_sr // => paux. move: (du_index_pr1 paux);rewrite Lgd => [[PQd]]; rewrite LgV //; move=> PPy Ppy. set (x:= J (P (P y)) (J (Q (P y)) (Q y))). have xs: (inc x (sum_of_substrates g)). rewrite /x;apply: disjoint_union_pi1 =>//. by rewrite - sr oa_link orsum_sr //; apply: disjoint_union_pi1. by ex_tac; rewrite /x ; aw; rewrite Ppy Qpy. rewrite /FF;hnf; split; fprops; first by saw; rewrite orsum_sr. hnf; aw;move=> x y xs ys; rewrite !LfV//. set gx := (J (J (P x) (P (Q x))) (Q (Q x))). set gy := (J (J (P y) (P (Q y))) (Q (Q y))). move: (du_index_pr1 xs)(du_index_pr1 ys) => [Qu Pu pu][Qv Pv pv]. move: Qu Qv;rewrite - sr oa_link (orsum_sr oa') => Qu Qv. move: (du_index_pr1 Qu)(du_index_pr1 Qv) => [QQx PQx pqu][QQy pQy pqv]. set P1:=inc gx (sum_of_substrates (Lg (domain g') F)). set P2:=inc gy (sum_of_substrates (Lg (domain g') F)). have p1p: P1. rewrite /P1; apply: disjoint_union_pi1; aw; trivial;rewrite LgV//. have Qs: inc (Q (Q x)) (substrate r') by ue. rewrite /F orsum_sr //; try apply: alo'' =>//. by apply: disjoint_union_pi1; [ rewrite Lgd // | aw; rewrite LgV // pqu]. have p2p: P2. rewrite /P2; apply: disjoint_union_pi1; aw; trivial. have Qs: inc (Q (Q y)) (substrate r') by ue. rewrite LgV// /F orsum_sr //; try apply: alo'' =>//. by apply: disjoint_union_pi1; [ rewrite Lgd // | rewrite LgV //pqv]. split; move /orsum_gleP => [_ _ h]; apply /orsum_gleP; split => //. have aux1: inc (Q (Q x)) (substrate r') by ue. hnf; rewrite /gx !pr1_pair !pr2_pair LgV//. move: (alo'' _ aux1) => aux2'. case: h. move => [] /orsum_gleP [Qx1 Qx2 hr] nxy. case: hr; first by left. move => [aa bb]; right; split => //; apply /orsum_gleP;split => //. by apply: disjoint_union_pi1; aw; trivial;rewrite LgV// pqu. by rewrite aa;apply: disjoint_union_pi1; aw; trivial;rewrite ! LgV// pqv. hnf; rewrite !pr2_pair (LgV PQx) !pr1_pair pqu. case: (equal_or_not (P (Q x)) (P (Q y)))=> aux5; last by left;split. by case: nxy; rewrite -pqu - pqv aa aux5. move=> [sq le1]; right;rewrite - sq; split => //. apply /orsum_gleP;split => //. by apply:disjoint_union_pi1; aw; trivial;rewrite LgV //pqu. by rewrite sq;apply: disjoint_union_pi1; aw; trivial;rewrite LgV// pqv. by right;hnf; aw; rewrite LgV// pqu. move:h;rewrite/order_sum_r /gx /gy !pr1_pair !pr2_pair; case. move=> [le ne] ; left; split; last by dneg ne1; ue. by apply /orsum_gleP;split => //; left. move=> [qq]; rewrite LgV //. have Qs: inc (Q (Q x)) (substrate r') by ue. move /orsum_gleP => [_ _]. rewrite/order_sum_r LgV//; aw; trivial. case; move => [hyp1 hyp2]. have aux2': Q x <> Q y by dneg ne1; ue. left; split => //; apply /orsum_gleP;split => //; right;split => //. right; split => //; first by apply: pair_exten. by move: hyp2; rewrite pqu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)