jubjub-subgroup-prime

(in-package "PRIMES")

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

(defprime jubjub-subgroup-prime
  6554484396890773809930967563523245729705921265872317281365359162392183254199
  (6 (2 3
      12281
      1710050753150114629
      203928654140967434528233
      255074062430788457494141376149)
    (1 1 1 1 1 1)
    (nil nil
      nil
      (6 (2 3 11 12954929948106929)
        (2 1 1 1)
        (nil nil
          nil
          (3 (2 23 35203613989421)
            (4 1 1)
            (nil nil
              (2 (2 5 1699 1036009829)
                (2 1 1 1)
                (nil nil
                  nil
                  (2 (2 7 499 74149) (2 1 1 1) (nil nil nil nil))))))))
      (5 (2 3 6566909 431305263804409)
        (3 2 1 1)
        (nil nil
          (2 (2 37 44371) (2 1 1) (nil nil nil))
          (13 (2 3 7 2567293236931)
            (3 1 1 1)
            (nil nil
              nil
              (2 (2 3 5 457 187256983)
                (1 1 1 1 1)
                (nil nil
                  nil
                  nil
                  (5 (2 3 11 2837227)
                    (1 1 1 1)
                    (nil nil
                      nil
                      (2 (2 3 7 43 1571) (1 1 1 1 1) (nil nil nil nil nil))))))))))
      (2 (2 3 311 5521 19861 623312455501769069)
        (2 1 1 1 1 1)
        (nil nil
          nil
          nil
          nil
          (2 (2 7 1361 16356472538621)
            (2 1 1 1)
            (nil nil
              nil
              (2 (2 5 23 62701 567097) (2 1 1 1 1) (nil nil nil nil nil)))))))))