proposition: Theorem NPEpow_ok e n : (e ^^ n === e ^ n)%poly.
proof: Proof. intros l. unfold NPEpow; destruct n. - simpl; now rewrite rpow_pow. - case Pos.eqb_spec; [intro; subst | intros _]. + simpl. now rewrite rpow_pow. + destruct e;simpl;trivial. repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl. * now rewrite phi_1, pow_pos_1. * now rewrite phi_0, pow_pos_0. * now rewrite pow_pos_cst. Qed.
imports: ZArith_base