proposition: Lemma BQmiddle_comp x y: x <q y -> x <q BQmiddle x y /\ BQmiddle x y <q y.
proof: Proof. move => cp. move: (cp) => [[xq yq _] _]. split. have : BQdouble x <q x +q y. by rewrite - (BQdouble_p xq); apply /(BQsum_lt2l xq yq xq). move /(BQprod_plt2r (QSdouble xq) (QSs xq yq) QpsSh2). by rewrite -/(BQhalf (BQdouble x)) (BQhalf_double xq). have : x +q y <q BQdouble y. by rewrite - (BQdouble_p yq); apply /(BQsum_lt2r xq yq yq). move /(BQprod_plt2r (QSs xq yq) (QSdouble yq) QpsSh2). by rewrite -/(BQhalf (BQdouble y)) (BQhalf_double yq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)