PA005D

predecessor_square_mod_one

Stable checked-use theorem · independently closed

The predecessor of a successor squares to one modulo that successor.

Exact expanded PA statement

forall p r. p = S r -> exists gs_u_square gs_v_square. (r * r) + p * gs_u_square = (1) + p * gs_v_square

Structural proof guide

Generated structural guide

The predecessor of a successor squares to one modulo that successor.

Use the direct prerequisites mul_one, mul_succ_left, add_assoc, add_comm, zero_add, add_succ_left as previously established PA formulas.

The proof proceeds by equality transport (2), certified simplification (1).

Referenced ingredients

PA0002 mul_one PA000G mul_succ_left PA0009 add_assoc PA000F add_comm PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0002 mul_one PA000G mul_succ_left PA0009 add_assoc PA000F add_comm PA0001 zero_add PA000E add_succ_left

Direct dependents

PA005E pow_predecessor_parity_mod PA00AP inverse_prefix_last_fixed

Formal 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.

  1. 0001intro p
  2. 0002intro r
  3. 0003intro hp
  4. 0004exists 1
  5. 0005exists r
  6. 0006rewrite hp
  7. 0007rewrite hp
  8. 0008simp [mul_one, mul_succ_left, add_assoc, add_comm, zero_add, add_succ_left]