proposition: Lemma Mphi_ok P (cM: C * Mon) l : let (c,M) := cM in let (Q,R) := MFactor P c M in P@l == Q@l + [c] * M@@l * R@l.
proof: Proof. destruct cM as (c,M). revert M l. induction P as [c0|p P ?|P2 ? ? P3 ?]; intros M; destruct M; intros l; simpl; auto; try (case ceqb_spec; intro He); try (case Pos.compare_spec; intros He); rewrite ?He; destr_factor; simpl; Esimpl. - assert (H := div_eucl_th div_th c0 c). destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. - assert (H := Mcphi_ok P c). destr_factor. Esimpl. - now rewrite <- jump_add, Pos.sub_add. - assert (H2 := Mcphi_ok P2 c). assert (H3 := Mcphi_ok P3 c). destr_factor. Esimpl. add_permut. - rewrite zmon_pred_ok. simpl. add_permut. - rewrite mkZmon_ok. simpl. add_permut. mul_permut. - add_permut. mul_permut. rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl. - rewrite mkZmon_ok. simpl. Esimpl. add_permut. mul_permut. rewrite <- pow_pos_add, Pos.sub_add by trivial; rsimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory