proposition: Lemma Ppow_N_ok l : (forall P, subst_l P@l == P@l) -> forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
proof: Proof. intros ? P n;destruct n;simpl. - reflexivity. - rewrite Ppow_pos_ok by trivial. Esimpl. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory