baby-jubjub-subgroup-prime

(in-package "PRIMES")

(include-book "kestrel/number-theory/defprime" :dir :system)

(defprime baby-jubjub-subgroup-prime
  2736030358979909402780800718157159386076813972158567259200215660948447373041
  (31 (2 3
      5
      11
      17
      967
      32151195060611136810608359
      178259130663561045147472537592047227885001)
    (4 1 1 2 1 1 1 1)
    (nil nil
      nil
      nil
      nil
      nil
      (3 (2 3 4139 431548080059745198929)
        (1 2 1 1)
        (nil nil
          nil
          (3 (2 7 19 202795150404015601)
            (4 1 1 1)
            (nil nil
              nil
              (7 (2 3 5 19 349 25485742523)
                (4 1 2 1 1 1)
                (nil nil
                  nil
                  nil
                  nil
                  (2 (2 43189 295049) (1 1 1) (nil nil nil))))))))
      (14 (2 3 5 6323 336157 1863691091902891838383581623)
        (3 2 4 1 1 1)
        (nil nil
          nil
          nil
          nil
          (5 (2 33409 27892051421815855583579)
            (1 1 1)
            (nil nil
              (2 (2 23 521 27743 513749 81654569)
                (1 1 1 1 1 1)
                (nil nil
                  nil
                  nil
                  nil
                  (3 (2 10206821)
                    (3 1)
                    (nil (2 (2 5 13 37 1061) (2 1 1 1 1) (nil nil nil nil nil)))))))))))))