proposition: Lemma monLift_lem : forall (n0 : nat) (b : mon (S n0)) (x : nat) (m : mon n0), b = c_n n0 x m -> {a : nat * mon n0 | b = monLift n0 a}.
proof: Proof. intros. rewrite H. exists (x, m). simpl in |- *. auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)