(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_236 imports Complex_Main begin theorem mathd_numbertheory_236: "(1999^2000) mod 5 = (1::nat)" sorry end