proposition: Lemma BRnpow_prop2 x y n : realp x -> realp y -> natp n -> (x*r y) ^r n = x ^r n *r y ^r n.
proof: Proof. move => xr yr. move: n; apply: Nat_induction; first by rewrite !BRnpowx0 (BRprod_1l RS1). move => n nN hr. by rewrite !(BRnpowxS _ nN) hr BRprod_ACA //; apply:RS_Brnpow. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)