(* Authors: Wenda Li *) theory mathd_numbertheory_543 imports Complex_Main "HOL-Computational_Algebra.Computational_Algebra" begin theorem mathd_numbertheory_543 : "(\ k \ ({n::nat. n dvd (30^4)}). 1) - 2 = (123::nat)" sorry end