proposition: Lemma QmsS_sum_rl x y: inc x BQms -> inc y BQms -> inc (x +q y) BQms.
proof: Proof. move => xqm yqm. move: (BQopp_negative1 xqm) (BQopp_negative1 yqm) => xz1 yz1. move: (BQms_sBQ xqm)(BQms_sBQ yqm) => xq yq. move:(QpsS_sum_rl xz1 yz1); rewrite - (BQoppD xq yq) => h. by move: (BQopp_K (QSs xq yq)) => <-; apply: BQopp_positive1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)