Exact expanded PA statement
forall a b. a + b = 0 -> b = 0Structural proof guide
Generated structural guide
A sum equal to zero has zero as its right addend.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1), equality transport (1).
Referenced ingredients
none
Proof neighborhood
Direct dependencies
none
Direct dependents
PA0006 beta_range_empty PA0007 mul_eq_zero PA000J add_eq_zero_left PA000N mul_eq_one_components PA0013 factor_difference PA001B le_zero PA002I bounded_beta_exclusive_recode_invariant PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0043 beta_repeat_empty PA004F finite_surjective_zero PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA0052 beta_product_replace_balance PA005L quadratic_residue_search_up_to PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007G beta_sign_factor_prefix_exists PA007L beta_pointwise_mul_prefix_exists PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008S prime_scaled_inverse_prefix_exists_bounded PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA00A6 prime_inverse_prefix_exists_bounded PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AB paired_inverse_witness_zero PA00BY beta_division_prefix_exists PA00CU beta_sum_replace_balance PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00E9 eisenstein_transposed_column_prefix_exists PA00EI eisenstein_transposed_column_count_prefix_exists PA00EX eisenstein_successor_row_split_prefix_existsFormal 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.