Exact expanded PA statement
forall p n i j. (((exists wip_strict_gap_symmetric_source_left_bound. wip_strict_gap_symmetric_source_left_bound + S i = n) /\ ((exists wip_strict_gap_symmetric_source_right_bound. wip_strict_gap_symmetric_source_right_bound + S j = n) /\ (exists wip_mod_left_symmetric_source_inverse wip_mod_right_symmetric_source_inverse. (S i) * S j + p * wip_mod_left_symmetric_source_inverse = 1 + p * wip_mod_right_symmetric_source_inverse)))) -> (((exists wip_strict_gap_symmetric_target_left_bound. wip_strict_gap_symmetric_target_left_bound + S j = n) /\ ((exists wip_strict_gap_symmetric_target_right_bound. wip_strict_gap_symmetric_target_right_bound + S i = n) /\ (exists wip_mod_left_symmetric_target_inverse wip_mod_right_symmetric_target_inverse. (S j) * S i + p * wip_mod_left_symmetric_target_inverse = 1 + p * wip_mod_right_symmetric_target_inverse))))Structural proof guide
Generated structural guide
The bounded inverse-index relation is symmetric.
Use the direct prerequisites mul_comm as previously established PA formulas.
The proof proceeds by case analysis (2), intermediate claims (1), equality transport (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 Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.