proposition: Theorem red_zerop : forall (a : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)), red (nf a P) P -> zerop (nf a P).
proof: Proof. unfold nf in |- *. intros p aP; case p. intros x c. case (Reducef A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os aP (exist (fun l => canonical A0 eqA ltM l) x c)); auto. unfold red in |- *; auto. intros x0; case x0. intros x1; case x1. simpl in |- *; auto. intros a l c0 H' H'0; inversion H'. simpl in |- *. change (reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec aP (mults (A:=A) multA (n:=n) (unit (mks A A0 eqA n ltM (a :: l) c0)) (a :: l)) (pO A n)) in H'0. inversion H'0. inversion H3. inversion H7. simpl in H0. cut (~ zeroP (A:=A) A0 eqA (n:=n) (unit (mks A A0 eqA n ltM (pX a l) c0))); [ intros nZd | idtac ]; auto. case (H0 (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (T1 A1 n) (b:=unit (mks A A0 eqA n ltM (pX a l) c0)) nZd) y)); auto. apply reduce_mults_invf with (1 := cs); auto. apply unit_T1; auto. apply unit_nZ; auto. Qed.
imports: Buchberger(moreCoefStructure)