theorem Hex.Conway.luebeckConwayPolynomial?_monic {p n : Nat} [ZMod64.Bounds p] {f : FpPoly p} (h : luebeckConwayPolynomial? p n = some f) : DensePoly.Monic f

Every successful lookup carries monic certification.