proposition: Theorem Field_simplify_eq_in_correct : forall 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 -> forall den, split (denum nfe1) (denum nfe2) = den -> forall np1, Nnorm n lmp (num nfe1 * right den) = np1 -> forall np2, Nnorm n lmp (num nfe2 * left den) = np2 -> FEeval l fe1 == FEeval l fe2 -> PCond l (condition nfe1 ++ condition nfe2) -> NPphi_dev l np1 == NPphi_dev l np2.
proof: Proof. intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). apply Field_simplify_aux_ok; trivial. Qed.
imports: ZArith_base