proposition: Theorem canonical_skip_fst : forall l a b, canonical (pX a (pX b l)) -> canonical (pX a l).
proof: Proof. Proof using os. intros l a b H'; split; auto. apply olist_imp_olist with (b := b); auto. inversion H'. generalize H0; simpl in |- *; intuition. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)