PD0012 · conservative definition

Mod4Three

n is three modulo four by an explicit quotient.

Readable signature

Mod4Three(n)

Exact expansion

exists h. n = 4 * h + 3

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