proposition: Lemma BZsum_pp x y: inc x BZp -> inc y BZp -> x +z y = BZ_of_nat ((BZ_val x) +c (BZ_val y)).
proof: Proof. have Hb := CS_sum2 (P x) (P y). move: CS0 => cs0 xp yp. by rewrite BZsumE /BZsum_v2 !Y_true; aw; fprops;rewrite csubn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)