proposition: Lemma nat_to_B_pow x y: nat_to_B (x ^ y) = nat_to_B x ^c nat_to_B y.
proof: Proof. elim: y =>[| n hrec /=]; first by rewrite cpowx0 //=; exact succ_zero. by rewrite (cpow_succ _ (nat_to_B_Nat n)) expnS nat_to_B_prod hrec cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)