proposition: Theorem red_cons : forall (a : poly A0 eqA ltM) (p : list (poly A0 eqA ltM)), In a p -> red a p.
proof: Proof. Proof using plusA os cs. intros a; case (seqp_dec A A0 eqA eqA_dec n ltM a spO). case a; unfold red, spO, seqP in |- *; simpl in |- *. intros x c H' p H'0; inversion H'; auto. apply reducestar_pO_is_pO with (p := x); auto. case a; unfold red, spO, seqP in |- *; simpl in |- *. intros x c H' p H'0. apply rstar_rtopO; auto. apply Rstar_n with (y := pO A n); auto. apply reduce_in_pO with (1 := cs); auto. change (inPolySet A A0 eqA n ltM (s2p A A0 eqA n ltM (exist (fun l : list (Term A n) => canonical A0 eqA ltM l) x c)) p) in |- *; apply In_inp_inPolySet; auto. red in |- *; intros H'2; apply H'; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply Rstar_0; auto. Qed.
imports: Buchberger(moreCoefStructure)