proposition: Lemma osum_distributive a b c: order a -> order b -> order c -> (order_prod2 c (order_sum2 a b)) \Is (order_sum2 (order_prod2 c a) (order_prod2 c b)).
proof: Proof. move=> oa ob oc. move: (orsum2_or oa ob) => oab. move: (orprod2_or oc oa) => oca. move: (orprod2_or oc ob) => ocb. move: (orprod2_or oc oab) => ocab. move:(orsum2_or oca ocb) => ocacb. set (f := fun z => J (variantLc (P (Vg z C0)) (Vg z C1)) (Q (Vg z C0))). set A := substrate a; set B := substrate b; set C := substrate c. set E:= substrate (order_prod2 c (order_sum2 a b)). set F:= substrate(order_sum2 (order_prod2 c a)(order_prod2 c b)). have Ep: E = product2 (canonical_du2 A B) C. rewrite /E orprod2_sr // orsum2_sr //. have Fp: F = canonical_du2 (product2 A C)(product2 B C). rewrite /F orsum2_sr // !orprod2_sr //. have Ev: forall x, inc x E <-> [/\ fgraph x, domain x = C2, pairp (Vg x C0), ((inc (P (Vg x C0)) A /\ Q (Vg x C0) = C0) \/ (inc (P (Vg x C0)) B /\ Q (Vg x C0) = C1)) &inc (Vg x C1) C]. move=> x; rewrite Ep; split. move /setX2_P => [pa pb pc pd]; move/candu2P: pc => [pe] [] [pf pg]; split => //; [left | right ]; split => //. by move => [pa pb pc pd pe]; apply /setX2_P;split => //; apply/candu2P. have Fv: forall x, inc x F <-> [/\ pairp x, fgraph (P x), domain (P x) = C2, inc (Vg (P x) C1) C & ((inc (Vg (P x) C0) A /\ Q x = C0) \/ (inc (Vg (P x) C0) B /\ Q x = C1))]. move=> x; rewrite Fp; split. move /candu2P => [pa []] [] /setX2_P [pb pc pd pe] pf; split;fprops. move => [pa pb pc pd];case; move =>[pe pf]; apply /candu2P;split => //; [left | right]; split => //;apply /setX2_P; split; fprops. have p1: forall x, inc x E -> inc (f x) F. move=> x /Ev [pa pb pc pd pe]; rewrite /f; apply/Fv; split; aww. have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move=> x y /Ev [fgx dx px hx qx] /Ev [fgy dy py hy qy]. rewrite /f => sf; move: (pr1_def sf)(pr2_def sf) => r1 r2. move: (f_equal (Vg ^~C0) r1)(f_equal (Vg ^~C1) r1); aw; move => r3 r4. apply: fgraph_exten =>//; [ ue | rewrite dx; move=> z zd; try_lvariant zd]. by apply: pair_exten. done. have p3: forall y, inc y F -> exists2 x, inc x E & y = f x. move=> y /Fv [py fPy dPy Vby Vay]. exists (variantLc (J (Vg (P y) C0) (Q y)) (Vg (P y) C1)). apply /Ev; aw; split; fprops. rewrite /f; aw; apply: pair_exten => //; [fprops | aw | by aw ]. apply: fgraph_exten; [ exact| fprops | by aw | aw]. by rewrite dPy; move=> x xtp; try_lvariant xtp; aw. exists (Lf f E F); saw; first by saw;apply: lf_bijective. red; aw;move=> x y xE yE; rewrite LfV // LfV //. have r1: Q (f x) = Q (Vg x C0) by rewrite /f pr2_pair. have r2: Q (f y) = Q (Vg y C0) by rewrite /f pr2_pair. have r3: Vg (P (f x)) C0 = P (Vg x C0) by rewrite /f; aw. have r4: Vg (P (f y)) C0 = P (Vg y C0) by rewrite /f; aw. have r5: Vg (P (f x)) C1 = Vg x C1 by rewrite /f; aw. have r6: Vg (P (f y)) C1 = Vg y C1 by rewrite /f; aw. have pa: pairp (Vg x C0) by move /Ev: xE => [_ _ px _]. have pb: pairp (Vg y C0) by move /Ev:yE => [_ _ px _]. move: (xE) => /Ev [fgx dx px hx qx]. move: (yE) => /Ev [fgy dy py hy qy]. move: C0_ne_C1 => nab. split. move /(orprod2_gleP oc oab) => [_ _ h]; apply /(orsum2_gleP). split; first by move: (p1 _ xE); rewrite /F orsum2_sr. by move: (p1 _ yE); rewrite /F orsum2_sr. rewrite r1 r2; case: h. move=> [q1 q2]; rewrite - q1. case: (equal_or_not (Q (Vg x C0)) C0)=> q3. case: hx; move=> [q4 q5]; last by case: nab ; rewrite - q3 - q5. constructor 1; rewrite q3; split => //. apply /(orprod2_gleP oc oa). split; first by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops; ue. left; rewrite r3 r4 r5 r6 q1; split =>//. constructor 2; split => //. case: hx; move=> [q4 q5]; first by case: q3. apply /(orprod2_gleP oc ob). split; first by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops; ue. left; rewrite r3 r4 r5 r6 - q1; split =>//. move => [] /(orsum2_gleP) [_ _ h1] h2; case: h1. move=> [q1 q2 q3]; constructor 1. split; [exact | exact | ]. case: hx; move=> [q4 q5]; last by case: nab; rewrite - q1 - q5. case: hy; move=> [q4' q5']; last by case: nab; rewrite - q2 - q5'. apply /(orprod2_gleP oc oa). split; first by apply/setX2_P; rewrite /f pr1_pair; aw; split;fprops. by apply/setX2_P; rewrite /f pr1_pair; aw; split;fprops. right; rewrite r3 r4;split => //;dneg aux. apply: pair_exten => //; ue. move => [q1 q2 q3]; constructor 2. case: hx; move=> [q4 q5]; first by case: q1. case: hy; move=> [q4' q5']; first by case: q2. split; [exact | exact | ]. apply /(orprod2_gleP oc ob). split; first by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops. by apply/setX2_P; rewrite /f pr1_pair; aw;split;fprops. right; rewrite r3 r4; split => // sP; case: h2. by apply: pair_exten => //; rewrite q5 q5'. move=> res; constructor 3; exact. move/(orsum2_gleP) => [_ _ h]; apply /(orprod2_gleP oc oab). split; first by move: xE; rewrite /E orprod2_sr //. by move: yE; rewrite /E orprod2_sr //. have pc: inc (Vg x C0) (canonical_du2 (substrate a) (substrate b)). by move: xE => /Ev [_ _ px' etc _]; apply/candu2P. have pd: inc (Vg y C0) (canonical_du2 (substrate a) (substrate b)). by move: yE => /Ev [_ _ px' etc _]; apply/candu2P. case: h. move=> [q1 q2] /(orprod2_gleP oc oa) [q3 q4]. rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ]. by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 q1 q2. split =>//; last by dneg neq; rewrite neq. by apply /orsum2_gleP;split => //; constructor 1;rewrite -r1 -r2 q1 q2. move=> [q1 q2] /(orprod2_gleP oc ob) [q3 q4]. case: hx; rewrite -r1; move => [_ sb]; first by case: q1. case: hy; rewrite -r2; move => [_ sb']; first by case: q2. rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ]. by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 sb sb'. split =>//; last by dneg neq; rewrite neq. apply /orsum2_gleP;split => //; constructor 2; rewrite - r1 -r2;split => //. move=> [q5 q6]; right; split. apply /orsum2_gleP;split => //; constructor 3; rewrite - r1 -r2;split => //. by dneg neq; rewrite r2 -neq -r1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)