proposition: Lemma fp_tail : forall x p, fP (p ++ x :: nil) = fP p ++ T2M x :: nil.
proof: Proof. intros x p; elim p; simpl in |- *; auto. intros a l H'; rewrite H'; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)