proposition: Theorem PFcons00_fcons_inv: forall l a l1, PCond l (Fcons00 a l1) -> ~ a @ l == 0 /\ PCond l l1.
proof: Proof. intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). - intros p H p0 H0 l1 H1. simpl in H1. destruct (H _ H1) as (H2,H3). destruct (H0 _ H3) as (H4,H5). split; trivial. simpl. apply field_is_integral_domain; trivial. - intros ? H ? ? H0. destruct (H _ H0). split; trivial. apply PEpow_nz; trivial. Qed.
imports: ZArith_base