proposition: Theorem Fnorm_FEeval_PEeval l fe: PCond l (condition (Fnorm fe)) -> FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l.
proof: Proof. induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n]; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; intros (Hc1,Hc2) || intros Hc; try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1); try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *. - now rewrite phi_1, phi_0, rdiv_def. - now rewrite phi_1; apply rdiv1. - rewrite phi_1; apply rdiv1. - rewrite phi_1; apply rdiv1. - rewrite NPEadd_ok, !NPEmul_ok. simpl. rewrite <- rdiv2b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial. now f_equiv. - rewrite NPEsub_ok, !NPEmul_ok. simpl. rewrite <- rdiv3b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial. now f_equiv. - rewrite !NPEmul_ok. simpl. rewrite IHfe1, IHfe2. rewrite (split_ok_l (num F1) (denum F2) l), (split_ok_r (num F1) (denum F2) l), (split_ok_l (num F2) (denum F1) l), (split_ok_r (num F2) (denum F1) l) in *. apply rdiv4b; trivial. - rewrite NPEopp_ok; simpl; rewrite (IHfe Hc); apply rdiv5. - rewrite (IHfe Hc2); apply rdiv6; trivial; apply Pcond_Fnorm; trivial. - destruct Hc2 as (Hc2,Hc3). rewrite !NPEmul_ok. simpl. assert (U1 := split_ok_l (num F1) (num F2) l). assert (U2 := split_ok_r (num F1) (num F2) l). assert (U3 := split_ok_l (denum F1) (denum F2) l). assert (U4 := split_ok_r (denum F1) (denum F2) l). rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4. simpl in U2, U3, U4. apply rdiv7b; rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial. - rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc). destruct n; simpl. + apply rdiv1. + apply pow_pos_div. apply Pcond_Fnorm; trivial. Qed.
imports: ZArith_base