proposition: Theorem PFcons1_fcons_inv: forall l a l1, PCond l (Fcons1 a l1) -> ~ a @ l == 0 /\ PCond l l1.
proof: Proof. intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). - simpl; intros c l1. case ceqb_spec'; intros H H0. + elim (@absurd_PCond_bottom l H0). + split; trivial. rewrite <- phi_0; trivial. - 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. - simpl; intros p H l1. case ceqb_spec'; intros H0 H1. + elim (@absurd_PCond_bottom l H1). + destruct (H _ H1). split; trivial. apply ropp_neq_0; trivial. rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial. - intros ? H ? ? H0. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. Qed.
imports: ZArith_base