proposition: Lemma oprod_assoc2 a b c: order a -> order b -> order c -> (order_prod2 a (order_prod2 b c)) \Is (order_prod2 (order_prod2 a b) c).
proof: Proof. move=> oa ob oc. have oab: order (order_prod2 a b) by apply: orprod2_or. have obc: order (order_prod2 b c) by apply: orprod2_or. set E:= substrate (order_prod2 a (order_prod2 b c)). set F:= substrate (order_prod2 (order_prod2 a b) c). set A:= substrate a; set B := substrate b; set C := substrate c. have Ev: E = product2 (product2 C B) A. by rewrite /E ! orprod2_sr. have Fv: F = product2 C (product2 B A). by rewrite /F ! orprod2_sr. have CB_pr: forall z, inc z (product2 C B) <-> [/\ fgraph z, domain z = C2, inc (Vg z C0) C & inc (Vg z C1) B]. by move=> z; apply /setX2_P. have BA_pr: forall z, inc z (product2 B A) <-> [/\ fgraph z, domain z = C2, inc (Vg z C0) B & inc (Vg z C1) A]. by move=> z; apply /setX2_P. set f := fun z => variantLc (Vg (Vg z C0) C0) (variantLc (Vg (Vg z C0) C1) (Vg z C1)). have p01: forall x, inc x E -> inc (f x) F. move=> x; rewrite Ev Fv; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. rewrite /f; aw; apply /setX2_P; split => //; aww. by apply /setX2_P; split;fprops; aw. have p02: forall x y, inc x E -> inc y E -> f x = f y -> x = y. move=> x y; rewrite Ev; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. rewrite /f; move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'] sf. move: (f_equal (Vg ^~ C0) sf) (f_equal (Vg ^~C1) sf); aw => sf1 sf2. move: (f_equal (Vg ^~C0) sf2) (f_equal (Vg ^~C1) sf2); aw => sf3 sf4. apply: fgraph_exten =>//; try ue. rewrite p2; move=> z zdx;try_lvariant zdx; trivial. apply: fgraph_exten =>//; try ue. by rewrite p5; move=> zz zdx; try_lvariant zdx. have p03: forall y, inc y F -> exists2 x, inc x E & y = f x. move=> y; rewrite Fv; move /setX2_P => [p1 p2 p3 /setX2_P [p4 p5 p6 p7]]. exists (variantLc (variantLc (Vg y C0) (Vg (Vg y C1) C0)) (Vg (Vg y C1) C1)). rewrite Ev;apply /setX2_P; split;aww. by apply /setX2_P; split;fprops; aw. rewrite /f; symmetry;apply: fgraph_exten => //; aww. move=> x xtp; try_lvariant xtp; trivial. apply: fgraph_exten => //; aw ; [fprops | by symmetry | ]. by move=> z xtp; try_lvariant xtp. exists (Lf f E F); split => //; fprops;aw. by apply: orprod2_or. by apply: orprod2_or. saw;apply: lf_bijective => //. red; aw; move=> x y xE yE; rewrite ! LfV //. move: (xE); rewrite Ev;move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3]. move: (yE);rewrite Ev;move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3']. split. move: (p01 _ xE)(p01 _ yE) => xF yF. move: xF; rewrite Fv; case /setX2_P=>[q1 q2 q3 /setX2_P [q4 q5 q6 q7]]. move: yF; rewrite Fv; case /setX2_P=>[r1 r2 r3 /setX2_P [r4 r5 r6 r7]]. have x1: inc (Vg (f x) C1) (product2 B A) by rewrite BA_pr. have y1: inc (Vg (f y) C1) (product2 B A) by rewrite BA_pr. set hi1:= inc (Vg (f x) C1) (product2 B A). set hi2:= inc (Vg (f y) C1) (product2 B A). move => tmp; apply /(orprod2_gleP oab oc). rewrite orprod2_sr // -/A -/B -/C -Fv;split => //; try apply: p01 => //. move: tmp => /(orprod2_gleP oa obc) [_ _]; case. move => [pa pb];left; split; first by rewrite /f;aw;ue. apply /(orprod2_gleP oa ob);split => //;left. by rewrite /f; aw;split => //; rewrite pa. move => [] /(orprod2_gleP ob oc) [_ _ aux'] nse. case: aux'; last by move=> aux2; right; rewrite /f; aw. move=> [Vaa Vba]; left; split; first by rewrite /f; aw. apply /(orprod2_gleP oa ob);split => //; right. rewrite /f ! LgV//; aww; split => //; dneg aux3. apply: fgraph_exten =>//; try ue. by rewrite p5; move=> z zd; try_lvariant zd. move /(orprod2_gleP oab oc) => [_ _ tmp]. apply/(orprod2_gleP oa obc); rewrite orprod2_sr // -/A -/B -/C -Ev;split => //. have x1: inc (Vg x C0) (product2 C B) by rewrite CB_pr. have y1: inc (Vg y C0) (product2 C B) by rewrite CB_pr. case: tmp; last first. rewrite /f; aw; move=> [h1 h2]; right; split. apply /(orprod2_gleP ob oc);split => //; by right. by dneg eql; rewrite eql. rewrite /f; aw; move => [xaa] /(orprod2_gleP oa ob) [fxb fxa]; aw. case. move=> [sVab le]; left; split =>//. apply: fgraph_exten => //; first by ue. by rewrite p5; move=> z zd; try_lvariant zd. move=> [lt2 neq]; right;split; last by dneg aux; rewrite aux. by apply /(orprod2_gleP ob oc);split => //; left. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)