BT000L

add_eq_zero_right

Stable · empty-context checked

A sum equal to zero has zero as its right addend.

Exact expanded PA statement

forall a b. a + b = 0 -> b = 0

Structural proof guide

A sum equal to zero has zero as its right addend.

Direct prerequisites: none. The authored body proceeds by structural induction (1), equality transport (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT000M mul_eq_zero BT000Y le_zero BT001X add_eq_zero_left BT0020 mul_eq_one_components BT002G factor_difference 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 BT00S0 prime_power_quotient_prefix_exists BT00SF eisenstein_initial_segment_prefix_exists BT00SH division_successor_quotient_by_bit BT00T3 beta_pascal_zero_row_exists BT00T5 beta_pascal_row_step_exists BT00T7 beta_pascal_table_prefix_exists BT00TF beta_pascal_table_diagonal_boundary BT00U0 four_power_central_recurrence_step BT00U8 primorial_factor_prefix_exists BT00US primorial_interval_factor_prefix_exists BT00XX double_quotient_carry_prefix_exists BT00YQ prime_contribution_prefix_exists BT010L prime_contribution_interval_prefix_exists BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one BT0127 bertrand_strict

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002induction b
  3. 0003intro h
  4. 0004refl
  5. 0005intro h
  6. 0006exfalso
  7. 0007apply PA1
  8. 0008rewrite PA4 at h
  9. 0009exact h