proposition: Theorem not_double_canonical : forall (a : Term A n) (p : list (Term A n)), ~ canonical (pX a (pX a p)).
proof: Proof. Proof using os. intros a p; red in |- *; intros H'; try exact H'. absurd (ltT a a); auto. apply canonical_pX_order with (l := p); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)