proposition: Lemma PEpow_add_r (e : PExpr C) n n' : (e ^ (n+n') === e ^ n * e ^ n')%poly.
proof: Proof. intros l. simpl. rewrite !rpow_pow. destruct n; simpl. - rewrite rmul_1_l. trivial. - destruct n'; simpl. + rewrite rmul_1_r. trivial. + apply pow_pos_add_r. Qed.
imports: ZArith_base