proposition: Lemma BZsumA x y z: intp x -> intp y -> intp z -> x +z (y +z z) = (x +z y) +z z.
proof: Proof. move: x y z. pose f x := Yo (inc x BZp) (J \0c (P x)) (J (P x) \0c). pose g x := Yo ((P x) <=c (Q x)) (BZ_of_nat((Q x) -c (P x))) (BZm_of_nat ((P x) -c (Q x))). have Ha: forall x, inc x BZ -> g (f x) = x. move => x xz; rewrite /f/g; case: (inc_or_not x BZp) => h1; Ytac0; aw. move: (BZ_valN xz) => pa; move: (cle0n pa) => h2; Ytac0. by rewrite (cdiff_n0 pa); apply: BZp_hi_pr. case /BZ_i0P: xz => zt; last by []. move /indexed_P: (zt) => [_] /setC1_P [pa pb] _. have hh: ~(P x <=c \0c). by move => /cle0. by Ytac0 ;rewrite (cdiff_n0 pa); apply: BZm_hi_pr;apply:BZms_sBZm. set (NN:= Nat \times Nat). pose h x y := J ( (P x) +c (P y)) ( (Q x) +c (Q y)). have Hu: forall x y, inc x NN -> inc y NN -> ((g x = g y) <-> ( (P x) +c (Q y) = (P y) +c (Q x))). move => x y /setX_P [_ pa pb] /setX_P [_ pc pd]; rewrite /g. case:(cleT_el (CS_nat pa)(CS_nat pb)) => h1; case:(cleT_el (CS_nat pc)(CS_nat pd)) => h2. - Ytac0; Ytac0; move: (cdiff_pr h1) (cdiff_pr h2). set a:= Q x -c P x; set b:= Q y -c P y; move => eqa eqb. rewrite /BZ_of_nat; split => ha. by rewrite - eqa -eqb (pr1_def ha) csumA (csumA (P y)) (csumC (P y)). congr (J _ C1); move: ha; rewrite -eqa csumA - eqb csumA (csumC (P x)). move => t; symmetry;apply:(csum_eq2l (NS_sum pc pa) _ _ t); rewrite /a /b; fprops. - have h3:=(cltNge h2). move: (cdiff_nz h2) => h4. Ytac0; Ytac0; rewrite /BZ_of_nat /BZm_of_nat; Ytac0; split => h5. by case: C1_ne_C0; move: (pr2_def h5). by move: (csum_Mlelt pb h1 h2); rewrite h5 csumC; move => [_]. - have h3:=(cltNge h1). move: (cdiff_nz h1) => h4. Ytac0; Ytac0; rewrite /BZ_of_nat /BZm_of_nat; Ytac0; split => h5. by case: C1_ne_C0; move: (pr2_def h5). by move: (csum_Mlelt pd h2 h1); rewrite - h5 csumC; move => [_]. - have h3:=(cltNge h1). have h4:=(cltNge h2). move: (cdiff_nz h2) => h5. move: (cdiff_nz h1) => h6. Ytac0; Ytac0; rewrite /BZm_of_nat; Ytac0; Ytac0. move: (cdiff_pr(proj1 h1)) (cdiff_pr (proj1 h2)). set a:= P x -c Q x; set b:= P y -c Q y; move => eqa eqb. split => ha. by rewrite - eqa -eqb (pr1_def ha) - csumA csumC (csumC b). congr (J _ C0); move: ha; rewrite -eqa csumC csumA - eqb. rewrite (csumC _ b) - (csumA b) (csumC (Q y)) (csumC b) => t. apply:(csum_eq2l (NS_sum pb pd) _ _ t); rewrite /a /b; fprops. have H: (forall x y, intp x -> intp y -> x +z y = g (h (f x) (f y))). by move => x y xi yi; rewrite BZsumE BZsum_alt. have Hf:forall x, inc x BZ -> inc (f x) NN. move => x xz; move: (BZ_valN xz) => pb. rewrite /f; Ytac t; apply: setXp_i => //; apply: NS0. have Hg:forall x, inc x NN -> inc (g x) BZ. move => x /setX_P [_ pa pb]; rewrite /g; Ytac aux. by apply: BZ_of_nat_i; apply:NS_diff. by apply: BZm_of_nat_i; apply:NS_diff. have Hh:forall u v, inc u NN -> inc v NN -> inc (h u v) NN. move => u v /setX_P [_ pa pb] /setX_P [_ pc pd]. by apply: setXp_i; apply: NS_sum. move => x y z xZ yZ zZ; move: (ZSs xZ yZ) (ZSs yZ zZ). set (yz:= y +z z); set (xy:= x +z y) => xyZ yzZ. have : (g (f yz) = g (h (f y) (f z))) by rewrite Ha // /yz - (H _ _ yZ zZ). move /(Hu _ _ (Hf _ yzZ) (Hh _ _ (Hf _ yZ) (Hf _ zZ))) => eq1. have: (g (f xy) = g (h (f x) (f y))) by rewrite Ha // /xy - (H _ _ xZ yZ). move /(Hu _ _ (Hf _ xyZ) (Hh _ _ (Hf _ xZ) (Hf _ yZ))) => eq2. rewrite (H _ _ xZ yzZ) (H _ _ xyZ zZ). apply /(Hu _ _ (Hh _ _ (Hf _ xZ) (Hf _ yzZ)) (Hh _ _ (Hf _ xyZ) (Hf _ zZ))). move: eq1 eq2;rewrite /h !pr1_pair !pr2_pair. move: (Hf _ xZ) => /setX_P [_]. move: (Hf _ yZ) => /setX_P [_ ]. move: (Hf _ zZ) => /setX_P [_]. move: (Hf _ xyZ) => /setX_P [_ ]. move: (Hf _ yzZ) => /setX_P [_]. set (Px:= P (f x)); set (Qx:=Q (f x)); set (Py:= P (f y)); set (Qy:=Q (f y)). set (Pz:= P (f z)); set (Qz:=Q (f z)); set (Pyz:= P (f yz)). set (Qyz:= Q (f yz)) ; set (Pxy:= P (f xy)); set (Qxy:= Q (f xy)). move => pyzb qyzb pxyb qxyb pzb qzb pyb qyb pxb qxb eq1 eq2. apply: (csum_eq2r qyb); [ fprops | fprops |]. rewrite - csumA - csumA. set a := Pyz +c _. have -> : a = (Pyz +c (Qy +c Qz)) +c Qxy. rewrite /a - (csumA _ _ Qxy); congr (Pyz +c _). by rewrite csumC (csumC Qxy) csumA. set b := _ +c Qy. have -> : b = ((Pxy +c (Qx +c Qy)) +c Qyz) +c Pz. rewrite /b - !csumA; apply: f_equal. by rewrite csumC - !csumA (csumA Qyz Qy Pz) (csumC Qyz Qy) (csumA Qy Qyz Pz). rewrite eq1 eq2 - !csumA; apply: f_equal; apply: f_equal. by rewrite csumC (csumC _ Qxy) csumA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)