proposition: Lemma ZSs x y: intp x -> intp y -> intp (x +z y).
proof: Proof. move => xz yz; rewrite BZsumE /BZsum_v2. move: (BZ_valN xz)(BZ_valN yz) => pxn qxn. Ytac h1; first by apply:BZ_of_nat_i; apply:NS_sum. Ytac h2; first by apply:BZm_of_nat_i; apply:NS_sum. Ytac h3. by Ytac h4; [apply:BZ_of_nat_i | apply:BZm_of_nat_i]; apply: NS_diff. by Ytac h4; [apply:BZ_of_nat_i | apply:BZm_of_nat_i ];apply: NS_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)