proposition: Lemma BRnpow1n n : natp n -> \1r ^r n = \1r.
proof: Proof. move: n; apply: Nat_induction; first by rewrite BRnpowx0. by move => n nN hr; rewrite (BRnpowxS _ nN) hr (BRprod_1l RS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)