proposition: Lemma pow_pos_mul_r x p1 p2 : pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2.
proof: Proof. induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; simpl; trivial; ring [IHp1]. Qed.
imports: ZArith_base