proposition: Lemma keylem_cor : WR (A * B) (ProdRel A B leq R).
proof: Proof. Proof using wfgt wR declt. red in |- *; apply keylem with (bs := nil (A:=B)); auto. red in |- *; auto. apply nmin; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)