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

Every successful lookup carries irreducible certification.