The constant h_\mathbb{J} in [ZPS:5.4.9.3].
(jubjub-h) → h
Function: jubjub-h
(defun jubjub-h nil (declare (xargs :guard t)) (let ((__function__ 'jubjub-h)) (declare (ignorable __function__)) 8))
Theorem: natp-of-jubjub-h
(defthm natp-of-jubjub-h (b* ((h (jubjub-h))) (natp h)) :rule-classes :rewrite)
