proposition: Theorem canonical_cons : forall l a b, ltT b a -> ~ zeroP (A:=A) A0 eqA (n:=n) a -> canonical (pX b l) -> canonical (pX a (pX b l)).
proof: Proof. intros l a b H' H'0 H'1; split; simpl in |- *; auto. apply olist_cons; auto. repeat split; auto. inversion H'1; simpl in H0; intuition. apply canonical_nzeroP with (p := l); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)