proposition: Lemma fibr_prop7 x: realp x -> BRsquare x = \1r +r x -> forall n, natp n -> x ^r (csucc (csucc n)) = x ^r (csucc n) +r x ^r n.
proof: Proof. move => xr xrr n nN. have xnr := (RS_Brnpow xr nN). rewrite (BRnpowxS _ (NS_succ nN)) (BRnpowxS _ nN) BRprodA // -/(BRsquare _)xrr. by rewrite BRsumC (BRprodDl xnr xr RS1) BRprod_1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)