Readable signature
Mod4One(n)
Exact expansion
exists h. n = 4 * h + 1
This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
none
Used by definitions
none
Used by theorem statements or local proof propositions