proposition: Lemma fibr_prop1 a x y: realp x -> realp a -> realp y -> BRsquare y = a -> x = (\1r +r y) /r \2r -> BRsquare x = (a-r \1r)/r \4r +r x.
proof: Proof. move => xr ar yr syv ->. have ha: realp (\1r +r y) by apply:(RSs RS1). have hb:=(RSo RS1); have rs1 := RS1; have rs2 := RS2. have hd: realp (a -r \1r) by apply: RS_diff. rewrite (BRdiv_square ha RS2) (BRsum_square RS1 yr) syv {1}/BRsquare. rewrite (BRprod_1l RS1) (BRprod_1l yr). have ->: (\1r +r a) = (a -r \1r) +r BRdouble \1r. rewrite BRdouble_C - (BRdouble_s RS1) BRsumC BRsum_ACA // BRsum_opp_l //. by rewrite (BRsum_0r(RSs ar rs1)). rewrite - (BRsumA hd (RSdouble rs1) (RSdouble yr)) /BRdouble - BRprodDr //. rewrite (BRdiv_sumDl (RSp rs2 rs2) hd (RSp rs2 ha)) - BRprod_22. rewrite BRdiv_prod_simpl_l//; exact: BR2_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)