proposition: Lemma fibr_prop6 (x := (BRopp (BRinv BR_phi))): BRsquare x = \1r +r x.
proof: Proof. have ha:= (RS_inv RS_phi). have hb:= (RS_diff RS1 ha). have hc := (BRps_nz BRps_phi). rewrite /x /BRsquare (BRprod_opp_opp ha ha) -/(_ -r _). apply: (BRprod_eq2l (RSp ha ha) hb RS_phi hc). rewrite (BRprodBr RS_phi RS1 ha) (BRprod_1r RS_phi). rewrite (BRprodA RS_phi ha ha) (BRprod_inv1 RS_phi hc) (BRprod_1l ha). exact:fibr_prop4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)