proposition: Lemma QpsS_sum_r x y: inc x BQp -> inc y BQps -> inc (x +q y) BQps.
proof: Proof. move => /Zo_P [/BQ_P [_ _ pc _] pa] /Zo_P [/BQ_P [_ _ qc _] qa]. move:(ZpsS_prod pc qc) => dp. apply:BQ_of_pair_spos => //; apply:ZpsS_sum_r; last by apply:ZpsS_prod. by apply:ZpS_prod => //; apply: BZps_sBZp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)