proposition: Lemma POneSubst_ok P1 M1 P2 P3 l : POneSubst P1 M1 P2 = Some P3 -> M1@@l == P2@l -> P1@l == P3@l.
proof: Proof. unfold POneSubst. assert (H := Mphi_ok P1). destr_mfactor R1 S1. 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 Env BinPos BinNat BinInt Ring_theory