proposition: Lemma fibr_prop2 x y: realp x -> realp y -> BRsquare y = \5r -> x = (\1r +r y) /r \2r -> BRsquare x = \1r +r x.
proof: Proof. move => xr yr ha hb. rewrite (fibr_prop1 xr RS5 yr ha hb) BR_succ4 (BRdiff_sum1 RS1 RS4). by rewrite (BRdiv_xx RS4) //; move/ rlt0xP: RpsS4 => [_ /nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)