proposition: Lemma PNSubst1_ok n P1 cM1 P2 l : [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == (PNSubst1 P1 cM1 P2 n)@l.
proof: Proof. revert P1. induction n as [|n IHn]; simpl; intros P1; generalize (POneSubst_ok P1 cM1 P2); destruct POneSubst; intros; rewrite <- ?IHn; auto; reflexivity. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory