proposition: Lemma ZpsS_sum_r x y: inc x BZp -> inc y BZps -> inc (x +z y) BZps.
proof: Proof. move => pa pb. move: (pa) (pb) => /indexed_P [_ q1 _] /indexed_P [_ q2 _]. move /BZps_iP: pb => [pb pc];rewrite (BZsum_pp pa pb); apply /indexed_pi. apply: (BZsum_N_Ns q1 q2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)