proposition: Lemma PNSubst_ok n P1 cM1 P2 l P3 : PNSubst P1 cM1 P2 n = Some P3 -> [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l.
proof: Proof. unfold PNSubst. assert (H := POneSubst_ok P1 cM1 P2); destruct POneSubst; try discriminate. destruct n; inversion_clear 1. intros. rewrite <- PNSubst1_ok; auto. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory