proposition: Lemma Mcphi_ok P c l : let (Q,R) := CFactor P c in P@l == Q@l + [c] * R@l.
proof: Proof. revert l. induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. - assert (H := (div_eucl_th div_th) c0 c). destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. - destr_factor. Esimpl. - destr_factor. Esimpl. add_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory