proposition: Lemma QpS_sum x y: inc x BQp -> inc y BQp -> inc (x +q y) BQp.
proof: Proof. move => pa pb; case (equal_or_not y \0q) => h. by rewrite h BQsum_0r //; apply:(BQp_sBQ pa). by apply:BQps_sBQp; apply:QpsS_sum_r => //; apply/BQps_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)