proposition: Lemma BQdouble_half1 x: ratp x -> BQhalf x +q BQhalf x = x.
proof: Proof. move => h. by rewrite /BQhalf - (BQprodDr h QSh2 QSh2) BQdouble_half2 (BQprod_1r h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)