proposition: Theorem Field_correct n l lpe fe1 fe2 : Ninterp_PElist l lpe -> forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> Peq ceqb (Nnorm n lmp (num nfe1 * denum nfe2)) (Nnorm n lmp (num nfe2 * denum nfe1)) = true -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2.
proof: Proof. intros Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp. apply Fnorm_crossproduct; trivial. eapply ring_correct; eauto. Qed.
imports: ZArith_base