proposition: Lemma zRV_WR : WR (mon 0) (mdiv 0).
proof: Proof. red in |- *; red in |- *; apply Ind. intros a; apply Ind. intros a0; rewrite (monO_n0 a); rewrite (monO_n0 a0). apply Base; auto. apply FoundG; auto. apply FoundE; auto. apply mdiv_nil; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)