proposition: Theorem Field_simplify_eq_pow_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 -> NPphi_pow l (Nnorm n lmp (num nfe1 * right den)) == NPphi_pow l (Nnorm n lmp (num nfe2 * left den)) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2.
proof: Proof. intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond. apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial. simpl. rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3. rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3. simpl. rewrite !rmul_assoc. apply rmul_ext; trivial. rewrite (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl), (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl). rewrite Hlmp. apply Hcrossprod. Qed.
imports: ZArith_base