proposition: Lemma Eq_add_square A B: (coarse (dsum A B)) \Eq dsum (dsum (coarse A) (coarse B)) ((A \times B)\times C2).
proof: Proof. pose f x y fx fy := Yo (fx = C0) (Yo (fy = C0) (J (J (J x y) C0) C0) (J (J (J x y) C0) C1)) (Yo (fy = C0) (J (J (J y x) C1) C1) (J (J (J x y) C1) C0)). pose g := fun z => f (P (P z)) (P (Q z)) (Q (P z)) (Q (Q z)). exists (Lf g (coarse (dsum A B)) (dsum (dsum (coarse A) (coarse B)) ((A \times B) \times C2))). move:(set2_1 C0 C1) (set2_2 C0 C1); rewrite -/C2 => i1 i2. move: C0_ne_C1 C1_ne_C0 => C01 C10. saw; apply: lf_bijective. - move => t /setX_P [pt /candu2P [ha hb] /candu2P [hc hd]]. rewrite /g/f; case:hb =>- [hb ->];case:hd =>- [hd ->]; Ytac0; Ytac0. + by apply: candu2_pra; apply: candu2_pra; apply: setXp_i. + by Ytac0;apply: candu2_prb;apply: setXp_i => //;apply: setXp_i. + by apply: candu2_prb;apply: setXp_i => //;apply: setXp_i. + by apply: candu2_pra; apply: candu2_prb; apply: setXp_i. + rewrite/g/f; move => u v /setX_P [pt /candu2P [ha hb] /candu2P [hc hd]]. move => /setX_P [pt' /candu2P [ha' hb'] /candu2P [hc' hd']] h. rewrite - pt - pt' - ha -hc -ha' -hc'; move: h. case:hb =>- [hb ->];case:hd =>- [hd ->]; Ytac0; Ytac0; case:hb' =>- [hb' ->];case:hd' =>- [hd' ->]; Ytac0; Ytac0. + by move/pr1_def /pr1_def/pr12_def => [-> ->]. + by Ytac0; move /pr2_def =>h; case: C01. + by move /pr2_def =>h; case: C01. + by move /pr1_def /pr2_def =>h; case: C01. + by Ytac0; move/pr2_def => h ;case: C10. + by Ytac0;Ytac0;move/pr1_def /pr1_def/pr12_def => [-> ->]. + by Ytac0; move /pr1_def /pr2_def =>h; case: C01. + by Ytac0; move/pr2_def => h ;case: C10. + by move/pr2_def => h ;case: C10. + by Ytac0;move/pr1_def /pr2_def => h ;case: C10. + by move/pr1_def /pr1_def/pr12_def => [-> ->]. + by move/pr2_def => h ;case: C10. + by move/pr1_def /pr2_def => h ;case: C10. + by Ytac0; move /pr2_def =>h; case: C01. + by move /pr2_def =>h; case: C01. + by move/pr1_def /pr1_def/pr12_def => [-> ->]. move => y /candu2P [px]; case => - [qa qb]. case/candu2P: qa => ppy; case => - [ha hb]. move/setX_P: ha =>[c1 c2 c3]. exists (J (J (P (P (P y))) C0) (J (Q (P (P y))) C0)). by apply:setXp_i; apply:candu2_pra. by rewrite /g; aw; rewrite /f; Ytac0;Ytac0;rewrite c1 - {1} hb - qb ppy px. move/setX_P: ha =>[c1 c2 c3]. exists (J (J (P (P (P y))) C1) (J (Q (P (P y))) C1)). by apply:setXp_i; apply:candu2_prb. by rewrite /g; aw; rewrite /f; Ytac0; Ytac0;rewrite c1 - {1} hb - qb ppy px. move:qa=> /setX_P [py /setX_P [c1 c2 c3] /set2_P]; case => qq. exists (J (J (P (P (P y))) C0) (J (Q (P (P y))) C1)). by apply:setXp_i; [ apply:candu2_pra | apply:candu2_prb]. rewrite /g; aw; rewrite /f; Ytac0; Ytac0;Ytac0. by rewrite c1 - qq py - qb px. exists (J (J (Q (P (P y))) C1) (J (P (P (P y))) C0)). by apply:setXp_i; [ apply:candu2_prb | apply:candu2_pra]. rewrite /g; aw; rewrite /f; Ytac0; Ytac0. by rewrite -{2} qb c1 - qq py. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)