proposition: Lemma Ppow_pos_ok l : (forall P, subst_l P@l == P@l) -> forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.
proof: Proof. intros subst_l_ok res P p. revert res. induction p as [p IHp|p IHp|];simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; mul_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory