proposition: Lemma QpsS_prod a b: inc a BQps -> inc b BQps -> inc (a *q b) BQps.
proof: Proof. move => /Zo_P [/BQ_P [_ _ pb _ ] pa] /Zo_P [/BQ_P [_ _ qb _ ] qa]. by apply: BQ_of_pair_spos; apply:ZpsS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)