BT000D

succ_injective

Stable · empty-context checked

Successor is injective (the reusable PA2 lemma).

Exact expanded PA statement

forall n m. S n = S m -> n = m

Structural proof guide

Successor is injective (the reusable PA2 lemma).

Direct prerequisites: none. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

none

Direct dependents

BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TF beta_pascal_table_diagonal_boundary BT00TH beta_pascal_table_successor_cell_recurrence

Formal native tactic body

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

  1. 0001apply PA2