Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
forall n. 0 + n = nEvery purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. 0 + n = nProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA0002 mul_one PA000F add_comm PA000Q le_succ_self PA000W le_eq_or_lt PA0013 factor_difference PA0017 common_divisor_beta_moduli_divides_gap_times_c PA001A le_refl PA001C division_remainder_succ PA001K gcd_balanced_bezout_exists_up_to PA0021 dvd_to_mod_zero PA0026 binary_crt PA002E division_remainder_unique PA0034 beta_half_range_entry_bounds PA003E beta_at_self_of_bound PA005D predecessor_square_mod_one PA005L quadratic_residue_search_up_to PA005R quadratic_residue_bounded_equiv PA0065 factorial_succ_decompose PA0067 drop_add_prefix_from_fixed PA006Y odd_upper_remainder_reflection PA007C gauss_signed_half_magnitude_injective PA007V gauss_predecessor_half_range_aligned PA008F beta_range_one_entry_eq_succ PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00A2 prime_two_or_terminal_odd_shape PA00AP inverse_prefix_last_fixed PA00B2 prime_pair_order_paired_terminal_state_exists PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BG beta_range_two_product_is_factorial_succ PA00BN bounded_euler_criterion_dichotomy PA00BO double_predecessor_ne_one PA00BP odd_prime_one_not_mod_predecessor PA00BV arbitrary_gauss_lemma_complete PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00CL odd_reflected_remainder_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotientDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.