proposition: Theorem inPolySet_addEnd : forall (a : list (Term A n)) (p : poly A0 eqA ltM) (l : list (poly A0 eqA ltM)), inPolySet A A0 eqA n ltM a (addEnd p l) -> a = s2p A A0 eqA n ltM p \/ inPolySet A A0 eqA n ltM a l.
proof: Proof. intros a p l; elim l; simpl in |- *; auto. intros H'; inversion H'; auto. intros a0 l0 H' H'0; inversion H'0; auto. right. exact (incons A A0 eqA n ltM a1 p0 H l0). case H'; auto. intros H3; right; try assumption. apply inskip; auto. Qed.
imports: Buchberger(moreCoefStructure)