proposition: Lemma Mphi_ok P M l : let (Q,R) := MFactor P M in P@l == Q@l + M@@l * R@l.
proof: Proof. revert M l; induction P as [|? ? IHP|? IHP1 ? ? IHP2]; intros M; destruct M; intros l; simpl; auto; Esimpl. - case Pos.compare_spec; intros He; simpl. * destr_mfactor R1 S1. now rewrite IHP, He, !mkPinj_ok. * destr_mfactor R1 S1. rewrite IHP; simpl. now rewrite !mkPinj_ok, <- Mjump_add, Pos.add_comm, Pos.sub_add. * Esimpl. - destr_mfactor R1 S1. destr_mfactor R2 S2. rewrite IHP1, IHP2, !mkPX_ok, zmon_pred_ok; simpl; rsimpl. add_permut. - case Pos.compare_spec; intros He; simpl; destr_mfactor R1 S1; rewrite ?He, IHP1, mkPX_ok, ?mkZmon_ok; simpl; rsimpl; unfold tail; add_permut; mul_permut. * rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl. * rewrite mkPX_ok. simpl. Esimpl. mul_permut. rewrite <- pow_pos_add, Pos.sub_add by trivial; rsimpl. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory