proposition: Lemma addEnd_app : forall (a : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)), addEnd a P = P ++ a :: nil.
proof: Proof. intros a P; elim P; simpl in |- *; auto. intros a0 l H'; elim H'; auto. Qed.
imports: Buchberger(moreCoefStructure)