proposition: Lemma BRps_phi: inc BR_phi BRps.
proof: Proof. move:(BRsqrt_prop (BRps_sBRp RpsS5)) => [ha hb]. apply:BRhalf_pos; rewrite BRsumC;exact :(RpsS_sum_r hb RpsS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)