Algorithmic proofs of two theorems of Stafford

Two classical results of Stafford say that every (left) ideal of the n-thWeyl algebra An can be generated by two elements, and every holonomicAn-module is cyclic, i.e. generated by one element. We modify Stafford’s original proofs to make the algorithmic computation of these generators possible.