proposition: Lemma dicksonL : forall n : nat, WR (mon n) (mdiv n).
proof: Proof. intro. unfold WR in |- *. elim n. apply zRV_WR. intros. cut (WR (nat * mon n0) (ProdRel nat (mon n0) (leq nat lt) (mdiv n0))); [ intros | exact (keylem_cor nat (mon n0) lt (mdiv n0) lt_wf dec_lt X) ]. unfold WR in X0. change (GRBar (mon (S n0)) (mdiv (S n0)) (map (monLift n0) nil)) in |- *. apply subRelGRBar with (R := ProdRel nat (mon n0) (leq nat lt) (mdiv n0)); auto. intros a b; case a; case b; simpl in |- *; auto. intros n1 m n2 m0 H'; inversion H'; auto. apply mdiv_cons; auto. apply leq2le; auto. intros b; exists (pmon1 (S n0) b, pmon2 (S n0) b); simpl in |- *. apply sym_eq; apply proj_ok; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)