proposition: Theorem addEnd_incl : forall (a : poly A0 eqA ltM) (L1 L2 : list (poly A0 eqA ltM)), incl (a :: L1) L2 -> incl (addEnd A A0 eqA n ltM a L1) L2.
proof: Proof. unfold incl in |- *; simpl in |- *; auto. intros a L1 L2 H' a0 H'0. case (addEnd_cons A A0 eqA n ltM) with (1 := H'0); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)