Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded PA statement
forall c k d. (exists u. S (k * c) = d * u) -> (exists v. c = d * v) -> d = 1Structural proof guide
Generated structural guide
Every beta-shaped successor modulus is coprime to its base c.
Use the direct prerequisites divides_remainder, divisor_one, mul_comm as previously established PA formulas.
The proof proceeds by intermediate claims (2), certified simplification (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
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.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–5
02Establish hstepL6–7
03Establish h1L8–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divides remainder.
Original exact command ledger · 20 lines
- 0001
intro c - 0002
intro k - 0003
intro d - 0004
intro hm - 0005
intro hc - 0006
have hstep : S (k * c) = c * k + 1 - 0007
simp [mul_comm] - 0008
have h1 : exists w. 1 = d * w - 0009
specialize divides_remainder d - 0010
specialize divides_remainder (S (k * c)) - 0011
specialize divides_remainder c - 0012
specialize divides_remainder k - 0013
specialize divides_remainder 1 - 0014
apply divides_remainder - 0015
exact hm - 0016
exact hc - 0017
exact hstep - 0018
specialize divisor_one d - 0019
apply divisor_one - 0020
exact h1