proposition: Theorem T1_is_min_ltT : forall a, ~ ltT a (T1 A1 n).
proof: Proof. Proof using os. intros a; case a; unfold ltT in |- *; simpl in |- *; auto. intros a0 m; unfold M1 in |- *; apply (M1_min _ _ _ _ os); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)