proposition: Lemma POneSubst_ok P1 cM1 P2 P3 l : POneSubst P1 cM1 P2 = Some P3 -> [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l.
proof: Proof. destruct cM1 as (cc,M1). unfold POneSubst. assert (H := Mphi_ok P1 (cc, M1) l). simpl in H. destruct MFactor as (R1,S1); simpl. rewrite H. clear H. intros EQ EQ'. replace P3 with (R1 ++ P2 ** S1). - rewrite EQ', Padd_ok, Pmul_ok; rsimpl. - revert EQ. destruct S1; try now injection 1. case ceqb_spec; now inversion 2. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory