proposition: Lemma PEpow_mul_r (e : PExpr C) n n' : (e ^ (n * n') === (e ^ n) ^ n')%poly.
proof: Proof. intros l. simpl. rewrite !rpow_pow. destruct n, n'; simpl; trivial. - now rewrite pow_pos_1. - apply pow_pos_mul_r. Qed.
imports: ZArith_base