proposition: Theorem nf_irreducible : forall (p : poly A0 eqA ltM) (aP : list (poly A0 eqA ltM)), irreducible A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec aP (s2p A A0 eqA n ltM (nf p aP)).
proof: Proof. unfold nf in |- *. intros p aP; case (Reducef A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os aP p). intros x; case x; simpl in |- *; auto. intros x0 c H'; inversion H'. red in H0. red in |- *; red in |- *. intros q0; intros H'0; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) (unit (mks A A0 eqA n ltM x0 c))); [ intros nZd | idtac ]; auto. apply H0 with (q := 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 x0 c)) nZd) q0); auto. apply reduce_mults_invf with (1 := cs); auto. apply unit_T1; auto. apply unit_nZ; auto. Qed.
imports: Buchberger(moreCoefStructure)