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.