proposition: Theorem PFcons0_fcons_inv: forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1.
proof: Proof. intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0. - simpl; now split. - generalize (ring_correct O l nil a e). lazy zeta; simpl Peq. case Peq; intros H; rewrite !PCond_cons; intros (H1,H2); repeat split; trivial. + now rewrite H. + now apply IHl1. + now apply IHl1. Qed.
imports: ZArith_base