proposition: Lemma fibr_prop4: BRinv BR_phi = BR_phi -r \1r.
proof: Proof. have ha:= (RS_inv RS_phi). have hb:= (RS_diff RS_phi RS1). have hc := (BRps_nz BRps_phi). apply: (BRprod_eq2l ha hb RS_phi hc). rewrite (BRprod_inv1 RS_phi hc)(BRprodBr RS_phi RS_phi RS1)(BRprod_1r RS_phi). by rewrite -/(BRsquare _)fibr_prop3 (BRdiff_sum1 RS_phi RS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)