proposition: Lemma PolZadd_correct : forall P' P l, PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')).
proof: Proof. unfold PolZadd, PhiR. intros. simpl. refine (Padd_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