proposition: Lemma nat_of_exp_bin n (b : N) : n ^ b = pow_N 1 muln n b.
proof: Proof. by case: b; last (elim=> //= p <-; rewrite natTrecE mulnn -expnM muln2 ?expnS). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring