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