proposition: Theorem olist_cons : forall (l : list _) a b, ltT b a -> olist (pX b l) -> olist (pX a (pX b l)).
proof: Proof. intros l; pattern l in |- *; apply (rev_ind (A:=Term A n)); auto. intros x l0; case l0. simpl in |- *. unfold olist in |- *; simpl in |- *. intros H' a b H'0 H'1; try assumption. apply (d_conc _ ltM (T2M x) (T2M b) (consA (T2M a) nilA)). generalize (olist_ltT pO); unfold ltT, olist in |- *; simpl in |- *; auto. apply (olistOne a b); auto. intros b l1 H' a b0 H'0; generalize H'; pattern l1 in |- *; apply (rev_ind (A:=Term A n)); unfold ltT, olist in |- *; simpl in |- *; auto. intros H'2 H'3. apply (d_conc _ ltM (T2M x) (T2M b) (consA (T2M a) (consA (T2M b0) nilA))); auto. generalize (olist_ltT (b0 :: nil)); unfold ltT, olist in |- *; simpl in |- *; auto. simpl in |- *; apply H'2; auto. apply (desc_prefix _ ltM (consA (T2M b0) (consA (T2M b) nilA)) (T2M x)); auto. intros x1 l2; rewrite (fP_app (l2 ++ x1 :: nil) (x :: nil)); rewrite (fP_app l2 (x1 :: nil)); rewrite (fP_app l2 (x :: nil)). intros H'2 H'3 H'4; apply (d_conc _ ltM (T2M x) (T2M x1) (consA (T2M a) (consA (T2M b0) (consA (T2M b) (fP l2))))). generalize (olist_ltT (pX b0 (pX b l2))); unfold olist, ltT in |- *; intros H'5; apply H'5. rewrite (fP_app (pX b0 (pX b l2)) (pX x1 (pX x pO))); simpl in |- *; auto. generalize (sym_eq (app_assoc (fP l2) (consA (T2M x1) nilA) (consA (T2M x) nilA))); simpl in |- *; auto; unfold consA in |- *. intros H'6; rewrite <- H'6; simpl in |- *; auto. simpl in |- *; apply H'3; auto; apply (desc_prefix _ ltM) with (a := T2M x); auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)