PA003L

mod_eq_symm

Stable checked-use theorem · independently closed

Balanced natural congruence is symmetric.

Exact expanded PA statement

forall m a b. (exists u v. a + m * u = b + m * v) -> exists r s. b + m * r = a + m * s

Structural proof guide

Generated structural guide

Balanced natural congruence is symmetric.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA003R mod_eq_cancel_coprime PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0079 prime_scaled_same_target_unique PA0087 quadratic_residue_mod_equiv PA008E prime_mul_index_map_injective PA008M quadratic_residue_half_power_mod_one PA008O scaled_inverse_transport_right PA009C prime_scaled_inverse_unique PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete PA00C5 canonical_remainder_from_mod PA00CJ matching_parity_mod_two PA00D5 mod_two_zero_sum_to_congruent PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FL mod_two_preserves_parity

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 m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro h
  5. 0005cases h
  6. 0006cases h_witness
  7. 0007exists x1
  8. 0008exists x
  9. 0009symm
  10. 0010exact h_witness_witness