proposition: Theorem Pcond_Fnorm l e : PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0.
proof: Proof. induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n]; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. - simpl. rewrite phi_1; exact rI_neq_rO. - simpl. rewrite phi_1; exact rI_neq_rO. - simpl; intros. rewrite phi_1; exact rI_neq_rO. - simpl; intros. rewrite phi_1; exact rI_neq_rO. - rewrite <- split_ok_r. simpl. apply field_is_integral_domain. + apply split_nz_l, IHe1, Hc1. + apply IHe2, Hc2. - rewrite <- split_ok_r. simpl. apply field_is_integral_domain. + apply split_nz_l, IHe1, Hc1. + apply IHe2, Hc2. - simpl. apply field_is_integral_domain. + apply split_nz_r, IHe1, Hc1. + apply split_nz_r, IHe2, Hc2. - now apply IHe. - trivial. - destruct Hc2 as (Hc2,_). simpl. apply field_is_integral_domain. + apply split_nz_l, IHe1, Hc2. + apply split_nz_r, Hc1. - rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc. Qed.
imports: ZArith_base