proposition: Lemma ZmS_sum x y: inc x BZm -> inc y BZm -> inc (x +z y) BZm.
proof: Proof. case /setU1_P; first by move => pa pb; apply:BZms_sBZm; apply:ZmsS_sum_l. by move => -> h; rewrite BZsum_0l //; apply: BZm_sBZ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)