proposition: Lemma RS_Brnpow n: natp n -> realp (BRnpow n).
proof: Proof. move:n; apply:Nat_induction; first by rewrite BRnpowx0; exact:RS1. by move => n nN Hr; rewrite (BRnpowxS nN); apply: RSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)