proposition: Lemma osum_assoc2 a b c: order a -> order b -> order c -> (order_sum2 a (order_sum2 b c)) \Is (order_sum2 (order_sum2 a b) c).
proof: Proof. move=> oa ob oc. have oab: order (order_sum2 a b) by apply: orsum2_or. have obc: order (order_sum2 b c) by apply: orsum2_or. set E:= substrate (order_sum2 a (order_sum2 b c)). set F:= substrate (order_sum2 (order_sum2 a b) c). set A:= substrate a; set B := substrate b; set C := substrate c. have Ev: E = canonical_du2 A (canonical_du2 B C). by rewrite /E ! orsum2_sr. have Fv: F = canonical_du2 (canonical_du2 A B) C. by rewrite /F ! orsum2_sr. move: C1_ne_C0 => nT. move: C0_ne_C1 => nT1. set f := fun z => Yo (Q z = C0) (J (J (P z) C0) C0) (Yo (Q (P z) = C0) (J (J (P (P z)) C1) C0) (J (P (P z)) C1)). have p1: forall x, inc x E -> inc (f x) F. move => x; rewrite Ev Fv; move /candu2P => [px]; case. by move=> [PA Qa]; rewrite /f; Ytac0; apply: candu2_pra; apply: candu2_pra. move => [] /candu2P [pPx alt] Qb. have nQa: Q x <> C0 by rewrite Qb. rewrite /f; Ytac0. case: alt;move => [Ppx Qpx]. by Ytac0; apply: candu2_pra; apply: candu2_prb. rewrite (Y_false); [ apply: candu2_prb => // | rewrite Qpx; fprops]. have p2: forall y, inc y F -> exists2 x, inc x E & y = f x. move => y; rewrite Ev Fv; move /candu2P => [px]; case. move=> [] /candu2P [pPy aux] Qpy; case: aux. move=> [PPa QP]; exists (J (P (P y)) C0). by apply: candu2_pra. rewrite /f pr2_pair; Ytac0; aw. apply: pair_exten =>//; fprops; aw; try ue. move=> [PPy QPy]; exists (J (J (P (P y)) C0) C1). by apply: candu2_prb; apply: candu2_pra. rewrite /f !(pr1_pair, pr2_pair); Ytac0; Ytac0. apply: pair_exten =>//; fprops; aw; try ue. move=> [Py Qy]; exists (J (J (P y) C1) C1). by apply: candu2_prb; apply: candu2_prb. rewrite /f !(pr2_pair, pr1_pair); Ytac0; Ytac0. apply: pair_exten =>//;aww. have p3: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move => x y; rewrite Ev; move /candu2P => [px hx] /candu2P [py hy]. rewrite /f;case: hx. move => [PxA Qxa]; Ytac0. case: hy. move => [PyA Qya]; Ytac0 => sf; move:(pr1_def sf). by rewrite - {1} Qxa - Qya px py. move=> [_ ] Qy; rewrite Qy; Ytac0; Ytac h1. move => h2;case: nT1; exact: (pr2_def(pr1_def h2)). move => h2;case: nT1; exact: (pr2_def h2). move => [] /candu2P [pPx auxx] Qx; rewrite Qx; Ytac0. case: hy. move=> [_ Qy]; Ytac0; Ytac h. move => h2;case: nT; exact: (pr2_def(pr1_def h2)). move => h2;case: nT; exact: (pr2_def h2). move=> [] /candu2P [pPy auxy] Qy; rewrite Qy; Ytac0. case: auxx; move=> [PPx Qpx]. Ytac0. case: auxy; move=> [PPy Qpy]. Ytac0 => sf; move: (pr1_def (pr1_def sf)) => sf1. apply: pair_exten =>//; try ue. apply: pair_exten =>//; try ue. rewrite Qpy;Ytac0=> sf; case: nT1; exact: (pr2_def sf). case: auxy; move=> [_ Qpy]. rewrite Qpx Qpy; Ytac0; Ytac0 => sf; case: nT; exact: (pr2_def sf). rewrite Qpx Qpy; Ytac0; Ytac0. move=> sf; move: (pr1_def sf) => sf1. apply: pair_exten =>//; try ue. apply: pair_exten =>//; try ue. exists (Lf f E F); split. by apply: orsum2_or. by apply: orsum2_or. rewrite ! orsum2_sr //; saw; first by apply: lf_bijective. red; rewrite lf_source;move=> x y xE yE; rewrite !LfV//. move: (xE); rewrite Ev ; move=> /candu2P [px hx]. move: (yE); rewrite Ev ; move=> /candu2P [py hy]. split. move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP; rewrite orsum2_sr //. split => //; first by move: (p1 _ xE); rewrite Fv. by move: (p1 _ yE); rewrite Fv. case: h. move=> [Qx Qy le]; constructor 1; rewrite /f (Y_true Qx) (Y_true Qy). rewrite ! pr1_pair ! pr2_pair; split => //. apply /orsum2_gleP;split => //; last by aw; constructor 1. apply candu2_pra; order_tac. apply candu2_pra; order_tac. move => [hxa hxb] /orsum2_gleP [_ _]. case: hx; move => [pxa qxa]; first by case: hxa. case: hy; move => [pya qya]; first by case: hxb. case; last first. by move => [sa sb]; constructor 3; rewrite /f; do 4 Ytac0; aw. by move => [sa sb sc];constructor 2; rewrite /f; do 4 Ytac0; aw. move => [sa sb sc]; constructor 1; rewrite /f; do 4 Ytac0; aw. case /candu2P: pxa => _ [] [ta tb]; last by case: nT; rewrite - sa - tb. case /candu2P: pya => _ [] [ta' tb']; last by case: nT; rewrite - sb - tb'. split => //; apply/orsum2_gleP; split => //. by apply: candu2_prb. by apply: candu2_prb. aw; by constructor 2. move=> [Qxa Qyb]. case: hy; move => [pya qya]; first by case: Qyb. case: hx; move => [pxa qxa]; last by case: nT; ue. move /candu2P: pya =>[_]; case; move => [sa sb]. constructor 1; rewrite /f; Ytac0; Ytac0; Ytac0; aw; split => //. apply /orsum2_gleP; split => //. - by apply candu2_pra. - by apply candu2_prb. - by constructor 3; aw. by constructor 3; rewrite /f sb; Ytac0; Ytac0; aw; Ytac0;aw. move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP. rewrite orsum2_sr // -/A -/B -/C - Ev;split => //. case: hx; move => [Px Qx]. have fx: f x = (J (J (P x) C0) C0) by rewrite /f Y_true. case: hy; move => [Py Qy]. have fy: f y = (J (J (P y) C0) C0) by rewrite /f Y_true. constructor 1; split => //. move: h; rewrite fx fy ! pr1_pair ! pr2_pair; case. - move=> [_ _] /orsum2_gleP [_ _]; case; aw; first by move => [_ _ s]. + by move=> [_ bad _]. + by move=> [_ bad]. - by move=> [_ bad _]. - by move=> [_ bad]. constructor 3; rewrite Qx Qy; split; exact. case: hy; move => [Py Qy]. case: (nT); case: h. move=> [Qfx Qfy] /orsum2_gleP [Pfx Pfy]. have -> : Q (P (f y)) = C0 by rewrite /f; Ytac0; aw. case; [ | move => [_ pa _] | move => [_ pa]]; try by case: pa. by move=> [h1 _]; move: h1 Qfx; rewrite /f Qx (Y_false) //;Ytac ww; aw. by move => [_ pa _]; move: pa; rewrite /f; Ytac0; aw. by move => [ _ ]; rewrite /f; Ytac0; aw. rewrite Qx Qy; constructor 2; split => //. apply /orsum2_gleP; split => //. move: Px Py => /candu2P [pPx hpx] /candu2P [pPy hpy]. case: hpx; move => [pa pb]. case: hpy; move => [pc pd]; last by constructor 3; rewrite pd;split => //. constructor 1; split => //; move: h; rewrite /f Qx Qy; do 4 Ytac0. case; [move => [_ _ ba] | move => [ba _] | move=> [_ ba]]; move: ba; aw => //. move /orsum2_gleP => [_ _];rewrite !pr1_pair !pr2_pair. by case; [ move => [sa _] | move => [_ _] | move => [sa _]]. constructor 2; rewrite pb; move: h; rewrite /f Qx Qy pb. Ytac0; Ytac0; Ytac0; case; first by move => [sa _]; move: sa; aw. Ytac ww; first by move => [_ qa _]; move: qa; aw. by move => [_ _]; aw. by move => [sa _]; move: sa; aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)