proposition: Lemma QmsS_sum_r x y: inc x BQm -> inc y BQms -> inc (x +q y) BQms.
proof: Proof. move => pa pb;case: (equal_or_not x \0q) => h. by rewrite h (BQsum_0l (BQms_sBQ pb)). by apply:QmsS_sum_rl => //; apply/BQms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)