PD0001

Le(a,b)

Witness-defined non-strict order on natural numbers.

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

Definition in prerequisite notation

a ≤ b

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

Hygienic expanded first-order definition 
exists h. h + a = b

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

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

none

Checked theorems using this definition

JT0015 · jordan_primitive_tuple_decidableJT0035 · jordan_rectangle_quotient_boundJT0036 · jordan_rectangle_flat_boundJT0042 · jordan_rectangle_crt_existsJT0049 · jordan_product_enumeration_existsJT0050 · jordan_enumeration_index_map_existsJT0053 · jordan_enumeration_cardinality_leJT0054 · jordan_enumeration_cardinality_unique