proposition: Theorem Field_rw_pow_correct n lpe l : Ninterp_PElist l lpe -> forall lmp, Nmk_monpol_list lpe = lmp -> forall fe nfe, Fnorm fe = nfe -> PCond l (condition nfe) -> FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
proof: Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). unfold display_pow_linear. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_pow_correct; eauto). destruct (ceqb_spec c cI) as [H0|]. - set (nnum := NPphi_pow _ _). apply eq_trans with (nnum / NPphi_pow l (Pc c)). + apply rdiv_ext; eapply ring_rw_pow_correct; eauto. + rewrite Pphi_pow_ok; try eassumption. now simpl; rewrite H0, phi_1, <- rdiv1. - apply rdiv_ext; eapply ring_rw_pow_correct; eauto. Qed.
imports: ZArith_base