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.
Exact expanded PA statement
forall n. n <= nStructural proof guide
Generated structural guide
The defined order is reflexive; zero is its witness.
Use the direct prerequisites zero_add as previously established PA formulas.
The proof proceeds by certified simplification (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA001L gcd_balanced_bezout_exists PA002G beta_exclusive_recode_congruence_step PA002X beta_prefix_extend PA0036 gcd_exists_relational PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA003Y beta_sum_succ_decompose PA0041 all_bits_last_succ PA004A beta_product_succ_decompose PA004D pow_successor_decompose PA004H finite_contains_decidable PA004I finite_bounded_last_succ PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA004U finite_swap_last_surjective_back PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded PA0051 beta_product_functional PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0065 factorial_succ_decompose PA006K beta_sum_trace_functional PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007I beta_sign_factor_product_power PA007N beta_product_pointwise_mul_exact PA007Q beta_product_pointwise_scale_mod PA007W beta_product_reindex_fixed_last PA007X beta_product_permutation_invariant PA0081 beta_product_pointwise_coprime PA008I prime_mul_residue_reindex_exists PA008T prime_scaled_inverse_prefix_exists PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA0097 finite_short_cover_impossible PA009K beta_prefix_append_two_exists PA009M beta_prefix_append_two_scaled_orbit_closed PA00A0 beta_adjacent_target_pairs_product_power PA00A7 prime_inverse_prefix_exists PA00AE finite_prefix_choose_unused_nonendpoint PA00AT beta_prefix_append_two_orbit_closed PA00B9 beta_adjacent_unit_pairs_product_one PA00BG beta_range_two_product_is_factorial_succ PA00CQ beta_sum_pointwise_mod_three_add PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant PA00CW beta_sum_reindex_fixed_last PA00CX beta_sum_permutation_invariant PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DL distinct_odd_prime_half_row_count_prefix_exists PA00DW beta_all_one_bit_count_exact PA00DX eisenstein_initial_segment_bit_count_functional PA00E9 eisenstein_transposed_column_prefix_exists PA00EE complementary_bit_counts_add_length PA00EI eisenstein_transposed_column_count_prefix_exists PA00EK beta_repeat_sum_exact PA00EP beta_sum_pointwise_add PA00EX eisenstein_successor_row_split_prefix_exists PA00F9 eisenstein_successor_terminal_bit_matches_last_column PA00FC eisenstein_fubini_universalFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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.
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n
02Construct an explicit witnessL2–2
Supply the displayed value, then prove that it has the required property.
- L2
exists 0
03Calculate and transport equalitiesL3–3
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L3
simp [zero_add]