proposition: Lemma BRnpow_prop1 n m: natp n -> natp m -> (BRnpow n) *r (BRnpow m) = (BRnpow (n +c m)).
proof: Proof. move => nN mN; move: n nN; apply: Nat_induction. by rewrite BRnpowx0 (csum0l (CS_nat mN)) (BRprod_1l (RS_Brnpow mN)). move => n nN h. rewrite (BRnpowxS nN) (csum_Sn _ nN)(BRnpowxS (NS_sum nN mN)) - h. symmetry; apply: (BRprodA xr (RS_Brnpow nN) (RS_Brnpow mN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)