Exact expanded PA statement
forall n. n <= nStructural proof guide
The defined order is reflexive; zero is its witness.
Direct prerequisites: zero_add. The authored body proceeds by direct introduction and elimination.
Proof neighborhood
Direct dependencies
Direct dependents
BT002V gcd_exists_relational BT0035 gcd_balanced_bezout_exists BT003E factor_search_up_to BT003L prime_divisor_exists BT005A beta_exclusive_recode_congruence_step BT005D beta_prefix_extend BT005E beta_prefix_product_trace_exists BT005G beta_product_functional BT005J beta_product_succ_decompose BT005K beta_product_succ_append BT0083 pow_successor_decompose BT0089 beta_prefix_sum_trace_exists BT008B beta_sum_trace_functional BT008F beta_sum_succ_decompose BT008K all_bits_last_succ BT0092 factorial_succ_decompose BT00DH beta_product_pointwise_coprime BT00JC beta_all_one_bit_count_exact BT00JD eisenstein_initial_segment_bit_count_functional BT00K5 beta_sum_pointwise_add BT00PR prime_strictly_above_decidable BT00PS bounded_prime_interval_search BT00PY pow_base_monotone BT00Q0 one_le_pow BT00Q5 bounded_power_valuation_search BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00T6 beta_pascal_table_prefix_extend BT00TC choose_functional BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TG choose_self BT00TI choose_succ_succ_of_lt BT00TJ choose_succ_succ BT00UD primorial_succ_decompose BT00UQ beta_product_prefix_suffix_split BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00VH primorial_odd_interval_divides_middle BT00VM central_binom_strong_upper_of_laws BT00VV primorial_le_four_pow_bounded BT00VW primorial_le_four_pow BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00X9 beta_product_pointwise_le BT00XX double_quotient_carry_prefix_exists BT00Y1 bit_count_positive_last_one BT00Y3 beta_sum_double_carry_exact BT010B floor_sqrt_two_le_of_two_lt BT010U beta_product_all_one_exact BT010W no_bertrand_middle_contribution_choice_le_selectorFormal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.