ND0231

FpNeg(p,a,b)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

An actual bounded additive inverse: FpAdd(p,a,b,0). Its existence and uniqueness are theorems.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

FpAdd(p,a,b,0)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
((exists pfa_gap_bottomlayeradditionleft. pfa_gap_bottomlayeradditionleft + S ((a)) = ((p))) /\ (((exists pfa_gap_bottomlayeradditionright. pfa_gap_bottomlayeradditionright + S ((b)) = ((p))) /\ ((((exists pfa_gap_bottomlayeradditionresultbound. pfa_gap_bottomlayeradditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_bottomlayeradditionresultcongruence pfa_offset_right_bottomlayeradditionresultcongruence. (((a)) + ((b))) + ((p)) * pfa_offset_left_bottomlayeradditionresultcongruence = (0) + ((p)) * pfa_offset_right_bottomlayeradditionresultcongruence))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

FpAdd(p,a,b,c)

Definitions depending on this notation

FpFieldLaws(p)FpNegPrefix(p,b,c,l)

Checked theorems using this definition

none directly; see definition consumers