proposition: Lemma ZmsS_sum_r x y: inc x BZm -> inc y BZms -> inc (x +z y) BZms.
proof: Proof. case /setU1_P; first by apply:ZmsS_sum_rl. by move => -> h; rewrite BZsum_0l //; apply: BZms_sBZ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)