proposition: Lemma ZmsS_sum_rl x y: inc x BZms -> inc y BZms -> inc (x +z y) BZms.
proof: Proof. move => xz yz. move: (BZopp_negative1 xz) (BZopp_negative1 yz) => xz1 yz1. move: (BZms_sBZ xz)(BZms_sBZ yz) => xz2 yz2. move: (ZpsS_sum_rl xz1 yz1); rewrite - (BZoppD xz2 yz2) => h. by move: (BZopp_K (ZSs xz2 yz2)) => <-; apply: BZopp_positive1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)