proposition: Lemma fibr_prop3: BRsquare BR_phi = \1r +r BR_phi.
proof: Proof. move:(BRsqrt_prop (BRps_sBRp RpsS5)) => [/esym ha hb]. apply:(fibr_prop2 (BRps_sBR BRps_phi) (BRp_sBR hb) ha); exact:BRhalf_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)