proposition: Lemma PolZmul_correct : forall P P' l, PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')).
proof: Proof. unfold PolZmul, PhiR. intros. refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext Rtheory) (gen_phiZ_morph Rset Rext Rtheory) _ _ _). Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia