proposition: Lemma BQhalf_pos1 x: inc x BQps -> (BQhalf x) <q x.
proof: Proof. move => h; move:(BQhalf_pos h) => h1. rewrite - {2} (BQdouble_half1 (BQps_sBQ h)). apply: (BQsum_Mps (BQps_sBQ h1) h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)