proposition: Lemma BRhalf_pos1 x: inc x BRps -> (BRhalf x) <r x.
proof: Proof. move => h; move:(BRhalf_pos h) => h1. rewrite - {2} (BRdouble_half1 (BRps_sBR h)). apply: (BRsum_Mps (BRps_sBR h1) h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)