fact: Definition mk_clean : forall a b : mon n, {c : mon n * bool | c = div_mon_clean n a b}.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)