proposition: Lemma BZsum_opp_r x: intp x -> x +z (BZopp x) = \0z.
proof: Proof. move => xz. wlog: x xz / inc x BZps. move => H;case /BZ_i1P: (xz). + by move => ->; rewrite BZopp_0 BZsum_0l //; apply: ZS0. + by apply: H. + move => xm; move: (BZopp_negative1 xm) => xm1. rewrite BZsumC - {2} (BZopp_K (BZms_sBZ xm));exact: (H _ (ZSo xz) xm1). move => yp; move: (BZopp_positive1 yp) => yp1. move: (BZps_sBZp yp) => yp2. case: (inc_or_not (BZopp x) BZp) => h1; first by case: (BZ_di_neg_pos yp1 h1). have ha: ~(inc x BZp /\ inc (BZopp x) BZp) by case. have hb: ~(~ inc x BZp /\ ~ inc (BZopp x) BZp) by case. rewrite BZsumE /BZsum_v2 (Y_false ha) (Y_false hb) (Y_true (conj yp2 h1)). by rewrite BZopp_val (Y_true (cleR (CS_nat (BZ_valN xz)))) cdiff_nn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)