proposition: Theorem nf_Cb : forall (a : poly A0 eqA ltM) (aP : list (poly A0 eqA ltM)), Cb a aP -> Cb (nf a aP) aP.
proof: Proof. intros a; case a; unfold nf, Cb in |- *; auto. intros x c Q H'; case (Reducef A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os Q (exist (fun l : list (Term A n) => canonical A0 eqA ltM l) x c)); auto. intros x0; case x0. intros x1 H'0 H'1. change (CombLinear A A0 eqA plusA multA eqA_dec n ltM ltM_dec Q (mults (A:=A) multA (n:=n) (unit (mks A A0 eqA n ltM x1 H'0)) x1)) in |- *. apply CombLinear_mults1 with (1 := cs); auto. apply unit_nZ; auto. apply reducestar_cb with (a := x) (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)