proposition: Lemma BZoppD x y: intp x -> intp y -> BZopp (x +z y) = (BZopp x) +z (BZopp y).
proof: Proof. pose R a b := BZopp (a +z b) = BZopp a +z BZopp b. have ha :forall a b, inc a BZps -> inc b BZms -> R a b. move => a b ap bn; rewrite /R. move: (BZps_sBZp ap) => ap1. rewrite (BZsum_pm ap1 bn). move: (BZ_valN (BZps_sBZ ap)) (BZ_valN (BZms_sBZ bn)) => pa pb. case: (equal_or_not (P a) (P b)) => pab. have hb: (BZopp b = a). by rewrite /BZopp /int_np -pab (BZms_sg bn); Ytac0; apply BZp_hi_pr. rewrite hb (BZsum_opp_l (BZps_sBZ ap)). rewrite Y_true pab; [ by rewrite cdiff_nn -/BZ_zero BZopp_0| fprops]. move: (BZopp_positive1 ap) (BZopp_negative1 bn) => nab nbc. rewrite BZsumC (BZsum_pm (BZps_sBZp nbc) nab) ! BZopp_val. case: (cleT_ee (CS_nat pb) (CS_nat pa)) => h. have h1: ~(P a <=c P b) by move => /(cleA h) ee; case: pab. by Ytac0; Ytac0; rewrite /BZ_of_nat /BZopp/int_np; aw; Ytac0. have h1: ~(P b <=c P a) by move => /(cleA h) ee; case: pab. move: (cdiff_nz (conj h pab)) => h2. by rewrite /BZopp /BZm_of_nat/int_np; Ytac0; Ytac0; Ytac0;aw; Ytac0; Ytac0. have hb :forall a b, inc a BZps -> inc b BZps -> R a b. move => a b pa pb. move: (BZopp_positive1 pa) (BZopp_positive1 pb) => n1 n2. move:(BZps_sBZp pa)(BZps_sBZp pb) => pa' pb'. rewrite /R BZsum_pp // BZsum_mm // ! BZopp_val. by rewrite /BZopp /BZ_of_nat/int_np; aw; Ytac0. have hc :forall a b, inc a BZps -> inc b BZ -> R a b. move => a b az bz; case /BZ_i1P: bz. + move: (BZps_sBZ az) => az1; move:(ZSo az1) => az2. move => ->; rewrite /R BZopp_0 !BZsum_0r //. + by move=> bz; apply: hb. + by move=> bz;apply: ha. move => xz yz; case /BZ_i1P: (xz) => xs. + by move:(ZSo yz) => yz2; rewrite xs /R BZopp_0 !BZsum_0l. + by apply: hc. + symmetry;rewrite - {2} (BZopp_K yz) - {2} (BZopp_K xz). move: (BZopp_negative1 xs) (ZSo xz) (ZSo yz) => xz1 xz2 yz1. by rewrite - (hc _ _ xz1 yz1) BZopp_K //; apply: ZSs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)