proposition: Theorem wf_incl : well_founded RO.
proof: Proof. unfold well_founded in |- *; intros. apply Acc_intro; intros. inversion H. apply l1 with (bs := nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a0 a :: nil) (ms := get_monL (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a0 a :: nil)); auto. change (GRBar (mon n) (mdiv n) (get_mon (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os a0 a) :: nil)) in |- *. apply nilGRBar; auto. apply dicksonL with (n := n); auto. simpl in |- *; intros f H3; case H3; intros. rewrite <- H4; auto. elim H4. red in |- *; intros H4; inversion H4; inversion H5. Qed.
imports: Coq(List) Buchberger(ListProps Bar Dickson Monomials)