proposition: Theorem Fnorm_ok: forall n l lpe fe, Ninterp_PElist l lpe -> Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true -> PCond l (condition (Fnorm fe)) -> FEeval l fe == 0.
proof: Proof. intros n l lpe fe Hlpe H H1. rewrite (Fnorm_FEeval_PEeval l fe H1). apply rdiv8. - apply Pcond_Fnorm; trivial. - transitivity (0@l); trivial. rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe); trivial. change (0 @ l) with (Pphi 0 radd rmul phi l (Pc cO)). apply (Peq_ok Rsth Reqe CRmorph); trivial. Qed.
imports: ZArith_base