Exact expanded PA statement
forall n. ~(S n = 0)Structural proof guide
No successor is zero (the reusable PA1 lemma).
Direct prerequisites: none. The authored body proceeds by direct introduction and elimination.
Proof neighborhood
Direct dependencies
none
Direct dependents
BT0022 mul_left_cancel_nonzero BT003E factor_search_up_to BT003G prime_nonzero BT003Y beta_modulus_nonzero BT004M bounded_common_multiple_step BT004N bounded_common_multiple_exists BT005C bounded_beta_exclusive_recode_invariant BT005E beta_prefix_product_trace_exists BT0069 beta_factor_divides_product BT007U beta_repeat_empty BT0084 beta_range_empty BT0089 beta_prefix_sum_trace_exists BT00R1 ceil_div_six_total BT00R9 square_lt_successor_square BT00RG double_triple_remainder_complement_budget BT00RK factorial_nonzero BT00RP prime_factorial_valuation_succ BT00S0 prime_power_quotient_prefix_exists BT00SF eisenstein_initial_segment_prefix_exists BT00SH division_successor_quotient_by_bit BT00SK power_quotient_successor_pointwise_add BT00T3 beta_pascal_zero_row_exists BT00T5 beta_pascal_row_step_exists BT00T7 beta_pascal_table_prefix_exists BT00T9 beta_pascal_zero_row_pointwise_functional BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TH beta_pascal_table_successor_cell_recurrence BT00U8 primorial_factor_prefix_exists BT00US primorial_interval_factor_prefix_exists BT00VB factorial_prime_le_of_divides BT00VK central_binom_strong_upper_step BT00WE ceil_div_six_budget_of_scaled_le BT00X1 six_block_window_decomposition_above_thirty_two BT00XX double_quotient_carry_prefix_exists BT00YQ prime_contribution_prefix_exists BT010L prime_contribution_interval_prefix_existsFormal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.
- 0001
apply PA1