proposition: Lemma BQ_double_plus x:ratp x -> BQdouble x +q x = \3q *q x.
proof: Proof. move => rx; rewrite -{2} (BQprod_1l rx) /BQdouble - (BQprodDl rx QS2 QS1). by rewrite (BQsum_cN NS2 NS1) - (Nsucc_rw NS2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)