PD0001

Le(a,b)

Witness-defined non-strict order on natural numbers.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

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

BetaZeroExtend(b,c,L,i,a)PolynomialPowerCoefficient(b,c,L,k,a)PolynomialQuotientLength(L,d,q)

Checked theorems using this definition

PG0035 · prime_field_polynomial_bounded_representative_at_length_existsPG0038 · prime_field_polynomial_common_representatives_at_length_existsPG0046 · prime_field_polynomial_aligned_add_cancel_leftPG0047 · prime_field_polynomial_aligned_add_associativePG0053 · prime_field_polynomial_division_remainder_length_descentPG0054 · prime_field_polynomial_division_constant_remainder_emptyPG0065 · prime_field_polynomial_reduced_representative_existsPG0069 · prime_field_polynomial_gcd_bezout_exists_up_toPG006D · prime_field_polynomial_nonzero_leading_equivalent_length_boundPG0071 · prime_field_polynomial_right_divides_represented_degree_bound