proposition: Lemma BZsum_0l x: intp x -> \0z +z x = x.
proof: Proof. move => xz; rewrite BZsumE /BZsum_v2. have cp:= (CS_nat (BZ_valN xz)). case: (p_or_not_p (inc x BZp)) => hx. rewrite (Y_true (conj ZpS0 hx)) /BZ_zero /BZ_of_nat; aw; rewrite csum0l//. exact:(BZp_hi_pr hx). have ha:= ZpS0. have hb: ~(inc \0z BZp /\ inc x BZp) by case. have hc: ~ (~ inc \0z BZp /\ ~ inc x BZp) by case. have hd: (inc \0z BZp /\ ~ inc x BZp) by split. Ytac0; Ytac0; Ytac0; rewrite /BZ_zero /BZ_of_nat; aww. rewrite (BZsum_spec cp) BZm_hi_pr //. by case/BZ_i0P: xz => // /BZms_sBZm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)