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