PA00BR · theorem

arbitrary_euler_criterion_residue_iff

Alpha v34 checked-use theorem · independently closed; not Stable

Euler's residue equivalence for an arbitrary nonmultiple representative.

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.

Statement with defined notation

∀ p. ∀ a. ∀ n. ∀ h. ∀ A. p = S n → Prime(p) → ¬Dvd(p,a) → n = h + h → Pow(a,h,A) → (QRes(p,a) → ModEq(p,A,1)) ∧ (ModEq(p,A,1) → QRes(p,a))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime PD0008 ModEq PD0020 Pow PD0021 QRes

7 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0020 Pow PD0021 QRes

17 occurrences

Exact expanded native-PA statement
forall p a n h A. p = S n -> ((~(p = 1) /\ forall frm_prime_left_eca_prime frm_prime_right_eca_prime. p = frm_prime_left_eca_prime * frm_prime_right_eca_prime -> frm_prime_left_eca_prime = 1 \/ frm_prime_right_eca_prime = 1)) -> (~(exists frm_factor_eca_not_divisor. a = p * frm_factor_eca_not_divisor)) -> n = h + h -> (exists ff_b_eca_power_endpoint ff_c_eca_power_endpoint. ((forall ff_i_eca_power_endpoint_repeat. (exists ff_lt_eca_power_endpoint_repeat_bound. ff_lt_eca_power_endpoint_repeat_bound + S ff_i_eca_power_endpoint_repeat = h) -> (((exists ff_h_eca_power_endpoint_repeat_decoded. ff_h_eca_power_endpoint_repeat_decoded + S (a) = S ((S (ff_i_eca_power_endpoint_repeat)) * ff_c_eca_power_endpoint)) /\ exists ff_q_eca_power_endpoint_repeat_decoded. ff_b_eca_power_endpoint = ff_q_eca_power_endpoint_repeat_decoded * S ((S (ff_i_eca_power_endpoint_repeat)) * ff_c_eca_power_endpoint) + (a)))) /\ (exists ff_u_eca_power_endpoint_product ff_v_eca_power_endpoint_product. ((((exists ff_h_eca_power_endpoint_product_start. ff_h_eca_power_endpoint_product_start + S (1) = S ((S (0)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_start. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_start * S ((S (0)) * ff_v_eca_power_endpoint_product) + (1))) /\ ((((exists ff_h_eca_power_endpoint_product_terminal. ff_h_eca_power_endpoint_product_terminal + S (A) = S ((S (h)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_terminal. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_terminal * S ((S (h)) * ff_v_eca_power_endpoint_product) + (A))) /\ forall ff_i_eca_power_endpoint_product. (exists ff_lt_eca_power_endpoint_product_bound. ff_lt_eca_power_endpoint_product_bound + S ff_i_eca_power_endpoint_product = h) -> exists ff_p_eca_power_endpoint_product ff_r_eca_power_endpoint_product ff_s_eca_power_endpoint_product. ((((exists ff_h_eca_power_endpoint_product_factor. ff_h_eca_power_endpoint_product_factor + S (ff_p_eca_power_endpoint_product) = S ((S (ff_i_eca_power_endpoint_product)) * ff_c_eca_power_endpoint)) /\ exists ff_q_eca_power_endpoint_product_factor. ff_b_eca_power_endpoint = ff_q_eca_power_endpoint_product_factor * S ((S (ff_i_eca_power_endpoint_product)) * ff_c_eca_power_endpoint) + (ff_p_eca_power_endpoint_product))) /\ ((((exists ff_h_eca_power_endpoint_product_partial. ff_h_eca_power_endpoint_product_partial + S (ff_r_eca_power_endpoint_product) = S ((S (ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_partial. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_partial * S ((S (ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product) + (ff_r_eca_power_endpoint_product))) /\ ((((exists ff_h_eca_power_endpoint_product_successor. ff_h_eca_power_endpoint_product_successor + S (ff_s_eca_power_endpoint_product) = S ((S (S ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_successor. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_successor * S ((S (S ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product) + (ff_s_eca_power_endpoint_product))) /\ ff_s_eca_power_endpoint_product = ff_r_eca_power_endpoint_product * ff_p_eca_power_endpoint_product)))))))) -> ((((exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a) -> (exists wpp_mod_left_eca_mod_one wpp_mod_right_eca_mod_one. (A) + p * wpp_mod_left_eca_mod_one = (1) + p * wpp_mod_right_eca_mod_one)) /\ ((exists wpp_mod_left_eca_mod_one wpp_mod_right_eca_mod_one. (A) + p * wpp_mod_left_eca_mod_one = (1) + p * wpp_mod_right_eca_mod_one) -> (exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a))))

Proof neighborhood

Direct theorem prerequisites

PA0031 prime_nonzero PA0086 nondivisor_canonical_remainder_exists PA0087 quadratic_residue_mod_equiv PA0088 pow_congruent_base_witness PA00BQ bounded_euler_criterion_residue_iff PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00BU arbitrary_euler_criterion_complete

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

92 script commands · 17 reading checkpoints · 10 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (7)
prime nonzeronondivisor canonical remainder existsquadratic residue mod equivpow congruent base witnessbounded euler criterion residue iffmod eq symmmod eq trans
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro h
  5. L5
    intro A
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotdiv
  9. L9
    intro heven
  10. L10
    intro hpower
02Establish hp0L11–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L11
    have hp0 : ~(p = 0)
  2. L12
    intro hpzero
  3. L13
    specialize prime_nonzero p
  4. L14
    apply prime_nonzero
  5. L15
    exact hp
  6. L16
    exact hpzero
03Establish hcanonicalL17–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nondivisor canonical remainder exists.

  1. L17
    have hcanonical : ∃ r. ¬r = 0 ∧ (Lt(r,p) ∧ ModEq(p,a,r))Definitions: Lt(r,p)ModEq(p,a,r)Original native command in the exact edition
  2. L18
    specialize nondivisor_canonical_remainder_exists p
  3. L19
    specialize nondivisor_canonical_remainder_exists a
  4. L20
    apply nondivisor_canonical_remainder_exists
  5. L21
    exact hp0
  6. L22
    exact hnotdiv
04Separate the logical casesL23–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    cases hcanonical
  2. L24
    cases hcanonical_witness
  3. L25
    cases hcanonical_witness_right
05Establish hpower_transportL26–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow congruent base witness.

  1. L26
    have hpower_transport : ∃ R. Pow(x,h,R) ∧ ModEq(p,A,R)Definitions: Pow(x,h,R)ModEq(p,A,R)Original native command in the exact edition
  2. L27
    specialize pow_congruent_base_witness p
  3. L28
    specialize pow_congruent_base_witness a
  4. L29
    specialize pow_congruent_base_witness x
  5. L30
    specialize pow_congruent_base_witness h
  6. L31
    specialize pow_congruent_base_witness A
  7. L32
    apply pow_congruent_base_witness
  8. L33
    exact hcanonical_witness_right_right
  9. L34
    exact hpower
06Separate the logical casesL35–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    cases hpower_transport
  2. L36
    cases hpower_transport_witness
07Establish hqres_equivL37–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply quadratic residue mod equiv.

  1. L37
    have hqres_equiv : (QRes(p,a) → QRes(p,x)) ∧ (QRes(p,x) → QRes(p,a))Definitions: QRes(p,a)QRes(p,x)Original native command in the exact edition
  2. L38
    specialize quadratic_residue_mod_equiv p
  3. L39
    specialize quadratic_residue_mod_equiv a
  4. L40
    specialize quadratic_residue_mod_equiv x
  5. L41
    apply quadratic_residue_mod_equiv
  6. L42
    exact hcanonical_witness_right_right
08Establish hboundedL43–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion residue iff.

  1. L43
    have hbounded : (QRes(p,x) → ModEq(p,x1,1)) ∧ (ModEq(p,x1,1) → QRes(p,x))Definitions: QRes(p,x)ModEq(p,x1,1)Original native command in the exact edition
  2. L44
    specialize bounded_euler_criterion_residue_iff p
  3. L45
    specialize bounded_euler_criterion_residue_iff x
  4. L46
    specialize bounded_euler_criterion_residue_iff n
  5. L47
    specialize bounded_euler_criterion_residue_iff h
  6. L48
    specialize bounded_euler_criterion_residue_iff x1
  7. L49
    apply bounded_euler_criterion_residue_iff
  8. L50
    exact hpn
  9. L51
    exact hp
  10. L52
    exact hcanonical_witness_left
09Use earlier factsL53–55

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    exact hcanonical_witness_right_left
  2. L54
    exact heven
  3. L55
    exact hpower_transport_witness_left
10Separate the logical casesL56–58

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L56
    cases hqres_equiv
  2. L57
    cases hbounded
  3. L58
    split
11Fix variables and assumptionsL59–59

Work with arbitrary variables or the premises of the current implication.

  1. L59
    intro hqa
12Establish hqrL60–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hqres equiv left.

  1. L60
  2. L61
    apply hqres_equiv_left
  3. L62
    exact hqa
13Establish hRoneL63–72

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbounded left.

  1. L63
    have hRone : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L64
    apply hbounded_left
  3. L65
    exact hqr
  4. L66
    specialize mod_eq_trans p
  5. L67
    specialize mod_eq_trans A
  6. L68
    specialize mod_eq_trans x1
  7. L69
    specialize mod_eq_trans 1
  8. L70
    apply mod_eq_trans
  9. L71
    exact hpower_transport_witness_right
  10. L72
    exact hRone
14Fix variables and assumptionsL73–73

Work with arbitrary variables or the premises of the current implication.

  1. L73
    intro hAone
15Establish hRAL74–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L74
  2. L75
    specialize mod_eq_symm p
  3. L76
    specialize mod_eq_symm A
  4. L77
    specialize mod_eq_symm x1
  5. L78
    apply mod_eq_symm
  6. L79
    exact hpower_transport_witness_right
16Establish hRoneL80–87

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L80
    have hRone : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L81
    specialize mod_eq_trans p
  3. L82
    specialize mod_eq_trans x1
  4. L83
    specialize mod_eq_trans A
  5. L84
    specialize mod_eq_trans 1
  6. L85
    apply mod_eq_trans
  7. L86
    exact hRA
  8. L87
    exact hAone
17Establish hqrL88–92

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbounded right.

  1. L88
  2. L89
    apply hbounded_right
  3. L90
    exact hRone
  4. L91
    apply hqres_equiv_right
  5. L92
    exact hqr

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009intro heven
  10. 0010intro hpower
  11. 0011have hp0 : ~(p = 0)
  12. 0012intro hpzero
  13. 0013specialize prime_nonzero p
  14. 0014apply prime_nonzero
  15. 0015exact hp
  16. 0016exact hpzero
  17. 0017have hcanonical : ∃ r. ¬r = 0 ∧ (Lt(r,p) ∧ ModEq(p,a,r))
    Exact native replay linehave hcanonical : exists r. ~(r = 0) /\ ((exists wpo_gap_eca_local_r_bound. wpo_gap_eca_local_r_bound + S (r) = p) /\ (exists wpp_mod_left_eca_local_a_r wpp_mod_right_eca_local_a_r. (a) + p * wpp_mod_left_eca_local_a_r = (r) + p * wpp_mod_right_eca_local_a_r))
  18. 0018specialize nondivisor_canonical_remainder_exists p
  19. 0019specialize nondivisor_canonical_remainder_exists a
  20. 0020apply nondivisor_canonical_remainder_exists
  21. 0021exact hp0
  22. 0022exact hnotdiv
  23. 0023cases hcanonical
  24. 0024cases hcanonical_witness
  25. 0025cases hcanonical_witness_right
  26. 0026have hpower_transport : ∃ R. Pow(x,h,R) ∧ ModEq(p,A,R)
    Exact native replay linehave hpower_transport : exists R. (exists ff_b_eca_proof_power_x_R ff_c_eca_proof_power_x_R. ((forall ff_i_eca_proof_power_x_R_repeat. (exists ff_lt_eca_proof_power_x_R_repeat_bound. ff_lt_eca_proof_power_x_R_repeat_bound + S ff_i_eca_proof_power_x_R_repeat = h) -> (((exists ff_h_eca_proof_power_x_R_repeat_decoded. ff_h_eca_proof_power_x_R_repeat_decoded + S (x) = S ((S (ff_i_eca_proof_power_x_R_repeat)) * ff_c_eca_proof_power_x_R)) /\ exists ff_q_eca_proof_power_x_R_repeat_decoded. ff_b_eca_proof_power_x_R = ff_q_eca_proof_power_x_R_repeat_decoded * S ((S (ff_i_eca_proof_power_x_R_repeat)) * ff_c_eca_proof_power_x_R) + (x)))) /\ (exists ff_u_eca_proof_power_x_R_product ff_v_eca_proof_power_x_R_product. ((((exists ff_h_eca_proof_power_x_R_product_start. ff_h_eca_proof_power_x_R_product_start + S (1) = S ((S (0)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_start. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_start * S ((S (0)) * ff_v_eca_proof_power_x_R_product) + (1))) /\ ((((exists ff_h_eca_proof_power_x_R_product_terminal. ff_h_eca_proof_power_x_R_product_terminal + S (R) = S ((S (h)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_terminal. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_terminal * S ((S (h)) * ff_v_eca_proof_power_x_R_product) + (R))) /\ forall ff_i_eca_proof_power_x_R_product. (exists ff_lt_eca_proof_power_x_R_product_bound. ff_lt_eca_proof_power_x_R_product_bound + S ff_i_eca_proof_power_x_R_product = h) -> exists ff_p_eca_proof_power_x_R_product ff_r_eca_proof_power_x_R_product ff_s_eca_proof_power_x_R_product. ((((exists ff_h_eca_proof_power_x_R_product_factor. ff_h_eca_proof_power_x_R_product_factor + S (ff_p_eca_proof_power_x_R_product) = S ((S (ff_i_eca_proof_power_x_R_product)) * ff_c_eca_proof_power_x_R)) /\ exists ff_q_eca_proof_power_x_R_product_factor. ff_b_eca_proof_power_x_R = ff_q_eca_proof_power_x_R_product_factor * S ((S (ff_i_eca_proof_power_x_R_product)) * ff_c_eca_proof_power_x_R) + (ff_p_eca_proof_power_x_R_product))) /\ ((((exists ff_h_eca_proof_power_x_R_product_partial. ff_h_eca_proof_power_x_R_product_partial + S (ff_r_eca_proof_power_x_R_product) = S ((S (ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_partial. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_partial * S ((S (ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product) + (ff_r_eca_proof_power_x_R_product))) /\ ((((exists ff_h_eca_proof_power_x_R_product_successor. ff_h_eca_proof_power_x_R_product_successor + S (ff_s_eca_proof_power_x_R_product) = S ((S (S ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_successor. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_successor * S ((S (S ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product) + (ff_s_eca_proof_power_x_R_product))) /\ ff_s_eca_proof_power_x_R_product = ff_r_eca_proof_power_x_R_product * ff_p_eca_proof_power_x_R_product)))))))) /\ (exists wpp_mod_left_eca_proof_A_R wpp_mod_right_eca_proof_A_R. (A) + p * wpp_mod_left_eca_proof_A_R = (R) + p * wpp_mod_right_eca_proof_A_R)
  27. 0027specialize pow_congruent_base_witness p
  28. 0028specialize pow_congruent_base_witness a
  29. 0029specialize pow_congruent_base_witness x
  30. 0030specialize pow_congruent_base_witness h
  31. 0031specialize pow_congruent_base_witness A
  32. 0032apply pow_congruent_base_witness
  33. 0033exact hcanonical_witness_right_right
  34. 0034exact hpower
  35. 0035cases hpower_transport
  36. 0036cases hpower_transport_witness
  37. 0037have hqres_equiv : (QRes(p,a) → QRes(p,x)) ∧ (QRes(p,x) → QRes(p,a))
    Exact native replay linehave hqres_equiv : (((exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a) -> (exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)) /\ ((exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x) -> (exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a)))
  38. 0038specialize quadratic_residue_mod_equiv p
  39. 0039specialize quadratic_residue_mod_equiv a
  40. 0040specialize quadratic_residue_mod_equiv x
  41. 0041apply quadratic_residue_mod_equiv
  42. 0042exact hcanonical_witness_right_right
  43. 0043have hbounded : (QRes(p,x) → ModEq(p,x1,1)) ∧ (ModEq(p,x1,1) → QRes(p,x))
    Exact native replay linehave hbounded : (((exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x) -> (exists wpp_mod_left_eca_proof_x1_one wpp_mod_right_eca_proof_x1_one. (x1) + p * wpp_mod_left_eca_proof_x1_one = (1) + p * wpp_mod_right_eca_proof_x1_one)) /\ ((exists wpp_mod_left_eca_proof_x1_one wpp_mod_right_eca_proof_x1_one. (x1) + p * wpp_mod_left_eca_proof_x1_one = (1) + p * wpp_mod_right_eca_proof_x1_one) -> (exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)))
  44. 0044specialize bounded_euler_criterion_residue_iff p
  45. 0045specialize bounded_euler_criterion_residue_iff x
  46. 0046specialize bounded_euler_criterion_residue_iff n
  47. 0047specialize bounded_euler_criterion_residue_iff h
  48. 0048specialize bounded_euler_criterion_residue_iff x1
  49. 0049apply bounded_euler_criterion_residue_iff
  50. 0050exact hpn
  51. 0051exact hp
  52. 0052exact hcanonical_witness_left
  53. 0053exact hcanonical_witness_right_left
  54. 0054exact heven
  55. 0055exact hpower_transport_witness_left
  56. 0056cases hqres_equiv
  57. 0057cases hbounded
  58. 0058split
  59. 0059intro hqa
  60. 0060have hqr : QRes(p,x)
    Exact native replay linehave hqr : exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x
  61. 0061apply hqres_equiv_left
  62. 0062exact hqa
  63. 0063have hRone : ModEq(p,x1,1)
    Exact native replay linehave hRone : exists wpp_mod_left_eca_proof_x1_one wpp_mod_right_eca_proof_x1_one. (x1) + p * wpp_mod_left_eca_proof_x1_one = (1) + p * wpp_mod_right_eca_proof_x1_one
  64. 0064apply hbounded_left
  65. 0065exact hqr
  66. 0066specialize mod_eq_trans p
  67. 0067specialize mod_eq_trans A
  68. 0068specialize mod_eq_trans x1
  69. 0069specialize mod_eq_trans 1
  70. 0070apply mod_eq_trans
  71. 0071exact hpower_transport_witness_right
  72. 0072exact hRone
  73. 0073intro hAone
  74. 0074have hRA : ModEq(p,x1,A)
    Exact native replay linehave hRA : exists wpp_mod_left_eca_proof_x1_A wpp_mod_right_eca_proof_x1_A. (x1) + p * wpp_mod_left_eca_proof_x1_A = (A) + p * wpp_mod_right_eca_proof_x1_A
  75. 0075specialize mod_eq_symm p
  76. 0076specialize mod_eq_symm A
  77. 0077specialize mod_eq_symm x1
  78. 0078apply mod_eq_symm
  79. 0079exact hpower_transport_witness_right
  80. 0080have hRone : ModEq(p,x1,1)
    Exact native replay linehave hRone : exists wpp_mod_left_eca_proof_x1_one wpp_mod_right_eca_proof_x1_one. (x1) + p * wpp_mod_left_eca_proof_x1_one = (1) + p * wpp_mod_right_eca_proof_x1_one
  81. 0081specialize mod_eq_trans p
  82. 0082specialize mod_eq_trans x1
  83. 0083specialize mod_eq_trans A
  84. 0084specialize mod_eq_trans 1
  85. 0085apply mod_eq_trans
  86. 0086exact hRA
  87. 0087exact hAone
  88. 0088have hqr : QRes(p,x)
    Exact native replay linehave hqr : exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x
  89. 0089apply hbounded_right
  90. 0090exact hRone
  91. 0091apply hqres_equiv_right
  92. 0092exact hqr