proposition: Lemma fibr_prop5: BR_phi +r BRinv BR_phi = BRsqrt \5r.
proof: Proof. move:(BRsqrt_prop (BRps_sBRp RpsS5)) => [_ /BRp_sBR hu]. have ha := RS_phi. have hb: realp (BRopp \1r) by apply: (RSo RS1). have hc:= (RSs RS1 hu). rewrite fibr_prop4 BRsumA // /BR_phi (BRdouble_half1 hc). exact:(BRdiff_sum RS1 hu). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)