proposition: Theorem nf_red : forall (a : poly A0 eqA ltM) (aP aQ : list (poly A0 eqA ltM)), incl aP aQ -> red (nf a aP) aQ -> red a aQ.
proof: Proof. intros a; case a; simpl in |- *. unfold red in |- *; unfold nf in |- *; simpl in |- *; auto. intros x c aP aQ H'; case (Reducef A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os aP (exist (fun a => canonical A0 eqA ltM a) x c)); simpl in |- *; auto. intros x0; case x0; simpl in |- *; auto. intros x1 c0 H'0 H'1. apply rstar_rtopO; auto. apply reduceplus_trans with (Q := aQ) (1 := cs) (y := x1); auto. inversion H'0; auto. apply inP_reduceplus with (Q := aP); auto. intros a0 H'3. apply Incl_inp_inPolySet with (P := aP); auto. apply reduceplus_mults_inv with (1 := cs) (a := unit (mks A A0 eqA n ltM x1 c0)); auto. apply unit_nZ; auto. apply unit_T1; auto. inversion H'1; inversion H; auto. Qed.
imports: Buchberger(moreCoefStructure)