proposition: Lemma BQdouble_p x : ratp x -> x +q x = BQdouble x.
proof: Proof. move => xq. rewrite - {1 2} (BQprod_1l xq) /BQdouble - BQsum_11 (BQprodDl) //; apply:QS1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)