proposition: Lemma PsubX_ok P' P k l : (forall P l, (P--P')@l == P@l - P'@l) -> (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k.
proof: Proof. intros IHP'. revert k l. induction P as [|p|? IHP1];simpl;intros. - rewrite Popp_ok;rsimpl; add_permut. - destruct p; simpl; rewrite Popp_ok;rsimpl; rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut. - destr_pos_sub; intros ->; Esimpl. + rewrite IHP';rsimpl. add_permut. + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + rewrite IHP1, pow_pos_add;rsimpl. add_permut. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory