PA0053 · theorem

beta_product_swap_last_invariant

Stable checked-use theorem · independently closed

Swapping an interior beta-coded factor with the last factor preserves the exact finite product.

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

∀ b. ∀ c. ∀ z. ∀ d. ∀ n. ∀ i. ∀ x. ∀ y. ∀ p. ∀ q. Lt(i,n) → BetaAt(b,c,i,x) → BetaAt(b,c,n,y) → BetaAt(z,d,i,y) → BetaAt(z,d,n,x) → (∀ m. ∀ k. Lt(m,S n) → ¬m = i → ¬m = n → BetaAt(b,c,m,k) → BetaAt(z,d,m,k)) → Product(b,c,S n,p) → Product(z,d,S n,q) → p = q

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

PD0002 Lt PD0013 BetaAt PD0014 Product

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product

7 occurrences

Exact expanded native-PA statement
forall b c z d n i x y p q. (exists h. h + S i = n) -> (((exists ff_h_product_swap_old_i. ff_h_product_swap_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_product_swap_old_i. b = ff_q_product_swap_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_product_swap_old_n. ff_h_product_swap_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_product_swap_old_n. b = ff_q_product_swap_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_product_swap_new_i. ff_h_product_swap_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_product_swap_new_i. z = ff_q_product_swap_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_product_swap_new_n. ff_h_product_swap_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_product_swap_new_n. z = ff_q_product_swap_new_n * S ((S (n)) * d) + (x))) -> (forall j a. (exists h. h + S j = S n) -> ~(j = i) -> ~(j = n) -> (((exists ff_h_product_swap_old_j. ff_h_product_swap_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_product_swap_old_j. b = ff_q_product_swap_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_product_swap_new_j. ff_h_product_swap_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_product_swap_new_j. z = ff_q_product_swap_new_j * S ((S (j)) * d) + (a)))) -> (exists ff_u_product_swap_old ff_v_product_swap_old. ((((exists ff_h_product_swap_old_start. ff_h_product_swap_old_start + S (1) = S ((S (0)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_start. ff_u_product_swap_old = ff_q_product_swap_old_start * S ((S (0)) * ff_v_product_swap_old) + (1))) /\ ((((exists ff_h_product_swap_old_terminal. ff_h_product_swap_old_terminal + S (p) = S ((S (S n)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_terminal. ff_u_product_swap_old = ff_q_product_swap_old_terminal * S ((S (S n)) * ff_v_product_swap_old) + (p))) /\ forall ff_i_product_swap_old. (exists ff_lt_product_swap_old_bound. ff_lt_product_swap_old_bound + S ff_i_product_swap_old = S n) -> exists ff_p_product_swap_old ff_r_product_swap_old ff_s_product_swap_old. ((((exists ff_h_product_swap_old_factor. ff_h_product_swap_old_factor + S (ff_p_product_swap_old) = S ((S (ff_i_product_swap_old)) * c)) /\ exists ff_q_product_swap_old_factor. b = ff_q_product_swap_old_factor * S ((S (ff_i_product_swap_old)) * c) + (ff_p_product_swap_old))) /\ ((((exists ff_h_product_swap_old_partial. ff_h_product_swap_old_partial + S (ff_r_product_swap_old) = S ((S (ff_i_product_swap_old)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_partial. ff_u_product_swap_old = ff_q_product_swap_old_partial * S ((S (ff_i_product_swap_old)) * ff_v_product_swap_old) + (ff_r_product_swap_old))) /\ ((((exists ff_h_product_swap_old_successor. ff_h_product_swap_old_successor + S (ff_s_product_swap_old) = S ((S (S ff_i_product_swap_old)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_successor. ff_u_product_swap_old = ff_q_product_swap_old_successor * S ((S (S ff_i_product_swap_old)) * ff_v_product_swap_old) + (ff_s_product_swap_old))) /\ ff_s_product_swap_old = ff_r_product_swap_old * ff_p_product_swap_old)))))) -> (exists ff_u_product_swap_new ff_v_product_swap_new. ((((exists ff_h_product_swap_new_start. ff_h_product_swap_new_start + S (1) = S ((S (0)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_start. ff_u_product_swap_new = ff_q_product_swap_new_start * S ((S (0)) * ff_v_product_swap_new) + (1))) /\ ((((exists ff_h_product_swap_new_terminal. ff_h_product_swap_new_terminal + S (q) = S ((S (S n)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_terminal. ff_u_product_swap_new = ff_q_product_swap_new_terminal * S ((S (S n)) * ff_v_product_swap_new) + (q))) /\ forall ff_i_product_swap_new. (exists ff_lt_product_swap_new_bound. ff_lt_product_swap_new_bound + S ff_i_product_swap_new = S n) -> exists ff_p_product_swap_new ff_r_product_swap_new ff_s_product_swap_new. ((((exists ff_h_product_swap_new_factor. ff_h_product_swap_new_factor + S (ff_p_product_swap_new) = S ((S (ff_i_product_swap_new)) * d)) /\ exists ff_q_product_swap_new_factor. z = ff_q_product_swap_new_factor * S ((S (ff_i_product_swap_new)) * d) + (ff_p_product_swap_new))) /\ ((((exists ff_h_product_swap_new_partial. ff_h_product_swap_new_partial + S (ff_r_product_swap_new) = S ((S (ff_i_product_swap_new)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_partial. ff_u_product_swap_new = ff_q_product_swap_new_partial * S ((S (ff_i_product_swap_new)) * ff_v_product_swap_new) + (ff_r_product_swap_new))) /\ ((((exists ff_h_product_swap_new_successor. ff_h_product_swap_new_successor + S (ff_s_product_swap_new) = S ((S (S ff_i_product_swap_new)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_successor. ff_u_product_swap_new = ff_q_product_swap_new_successor * S ((S (S ff_i_product_swap_new)) * ff_v_product_swap_new) + (ff_s_product_swap_new))) /\ ff_s_product_swap_new = ff_r_product_swap_new * ff_p_product_swap_new)))))) -> p = q

Proof neighborhood

Direct theorem prerequisites

PA0052 beta_product_replace_balance PA004A beta_product_succ_decompose PA002F beta_at_unique PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct theorem dependents

PA007X beta_product_permutation_invariant

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

102 script commands · 17 reading checkpoints · 6 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 (5)
beta product replace balancebeta product succ decomposebeta at uniquele succlt irrefl expanded
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro d
  5. L5
    intro n
  6. L6
    intro i
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro p
  10. L10
    intro q
02Fix variables and assumptionsL11–18

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

  1. L11
    intro hi
  2. L12
    intro hold_i
  3. L13
    intro hold_n
  4. L14
    intro hnew_i
  5. L15
    intro hnew_n
  6. L16
    intro hpreserve
  7. L17
    intro hproduct_old
  8. L18
    intro hproduct_new
03Establish hold_decompL19–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L19
    have hold_decomp : ∃ a. ∃ r. BetaAt(b,c,n,a) ∧ (Product(b,c,n,r) ∧ p = r · a)Definitions: BetaAt(b,c,n,a)Product(b,c,n,r)Original native command in the exact edition
  2. L20
    specialize beta_product_succ_decompose b
  3. L21
    specialize beta_product_succ_decompose c
  4. L22
    specialize beta_product_succ_decompose n
  5. L23
    specialize beta_product_succ_decompose p
  6. L24
    apply beta_product_succ_decompose
  7. L25
    exact hproduct_old
04Establish hnew_decompL26–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L26
    have hnew_decomp : ∃ a. ∃ r. BetaAt(z,d,n,a) ∧ (Product(z,d,n,r) ∧ q = r · a)Definitions: BetaAt(z,d,n,a)Product(z,d,n,r)Original native command in the exact edition
  2. L27
    specialize beta_product_succ_decompose z
  3. L28
    specialize beta_product_succ_decompose d
  4. L29
    specialize beta_product_succ_decompose n
  5. L30
    specialize beta_product_succ_decompose q
  6. L31
    apply beta_product_succ_decompose
  7. L32
    exact hproduct_new
05Separate the logical casesL33–40

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

  1. L33
    cases hold_decomp
  2. L34
    cases hold_decomp_witness
  3. L35
    cases hold_decomp_witness_witness
  4. L36
    cases hold_decomp_witness_witness_right
  5. L37
    cases hnew_decomp
  6. L38
    cases hnew_decomp_witness
  7. L39
    cases hnew_decomp_witness_witness
  8. L40
    cases hnew_decomp_witness_witness_right
06Establish hold_lastL41–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L41
    have hold_last : x1 = y
  2. L42
    specialize beta_at_unique b
  3. L43
    specialize beta_at_unique c
  4. L44
    specialize beta_at_unique n
  5. L45
    specialize beta_at_unique x1
  6. L46
    specialize beta_at_unique y
  7. L47
    apply beta_at_unique
  8. L48
    exact hold_decomp_witness_witness_left
  9. L49
    exact hold_n
07Establish hnew_lastL50–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L50
    have hnew_last : x3 = x
  2. L51
    specialize beta_at_unique z
  3. L52
    specialize beta_at_unique d
  4. L53
    specialize beta_at_unique n
  5. L54
    specialize beta_at_unique x3
  6. L55
    specialize beta_at_unique x
  7. L56
    apply beta_at_unique
  8. L57
    exact hnew_decomp_witness_witness_left
  9. L58
    exact hnew_n
08Establish hprefix_preserveL59–68

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

  1. L59
    have hprefix_preserve : ∀ j. ∀ a. Lt(j,n) → ¬j = i → BetaAt(b,c,j,a) → BetaAt(z,d,j,a)Definitions: Lt(j,n)BetaAt(b,c,j,a)BetaAt(z,d,j,a)Original native command in the exact edition
  2. L60
    intro j
  3. L61
    intro a
  4. L62
    intro hj
  5. L63
    intro hji
  6. L64
    intro hold
  7. L65
    specialize hpreserve j
  8. L66
    specialize hpreserve a
  9. L67
    apply hpreserve
  10. L68
    specialize le_succ (S j)
09Use earlier factsL69–72

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

  1. L69
    specialize le_succ n
  2. L70
    apply le_succ
  3. L71
    exact hj
  4. L72
    exact hji
10Fix variables and assumptionsL73–73

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

  1. L73
    intro hjn
11Use earlier factsL74–75

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

  1. L74
    specialize lt_irrefl_expanded n
  2. L75
    apply lt_irrefl_expanded
12Calculate and transport equalitiesL76–76

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L76
    rewrite hjn at hj
13Use earlier factsL77–78

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

  1. L77
    exact hj
  2. L78
    exact hold
14Establish hbalanceL79–88

Establish this local claim before using it. It is not an additional assumption.

  1. L79
    have hbalance : x4 * x = x2 * y
  2. L80
    specialize beta_product_replace_balance n
  3. L81
    specialize beta_product_replace_balance b
  4. L82
    specialize beta_product_replace_balance c
  5. L83
    specialize beta_product_replace_balance z
  6. L84
    specialize beta_product_replace_balance d
  7. L85
    specialize beta_product_replace_balance i
  8. L86
    specialize beta_product_replace_balance x
  9. L87
    specialize beta_product_replace_balance y
  10. L88
    specialize beta_product_replace_balance x2
15Use earlier factsL89–96

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

  1. L89
    specialize beta_product_replace_balance x4
  2. L90
    apply beta_product_replace_balance
  3. L91
    exact hi
  4. L92
    exact hold_i
  5. L93
    exact hnew_i
  6. L94
    exact hprefix_preserve
  7. L95
    exact hold_decomp_witness_witness_right_left
  8. L96
    exact hnew_decomp_witness_witness_right_left
16Calculate and transport equalitiesL97–101

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L97
    rewrite hold_decomp_witness_witness_right_right
  2. L98
    rewrite hnew_decomp_witness_witness_right_right
  3. L99
    rewrite hold_last
  4. L100
    rewrite hnew_last
  5. L101
    symm
17Use earlier factsL102–102

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

  1. L102
    exact hbalance

Library-wide reading audit

Original defined command ledger · 102 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro n
  6. 0006intro i
  7. 0007intro x
  8. 0008intro y
  9. 0009intro p
  10. 0010intro q
  11. 0011intro hi
  12. 0012intro hold_i
  13. 0013intro hold_n
  14. 0014intro hnew_i
  15. 0015intro hnew_n
  16. 0016intro hpreserve
  17. 0017intro hproduct_old
  18. 0018intro hproduct_new
  19. 0019have hold_decomp : ∃ a. ∃ r. BetaAt(b,c,n,a) ∧ (Product(b,c,n,r) ∧ p = r · a)
    Exact native replay linehave hold_decomp : exists a r. (((exists ff_h_swap_old_last. ff_h_swap_old_last + S (a) = S ((S (n)) * c)) /\ exists ff_q_swap_old_last. b = ff_q_swap_old_last * S ((S (n)) * c) + (a))) /\ ((exists ff_u_swap_old_prefix ff_v_swap_old_prefix. ((((exists ff_h_swap_old_prefix_start. ff_h_swap_old_prefix_start + S (1) = S ((S (0)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_start. ff_u_swap_old_prefix = ff_q_swap_old_prefix_start * S ((S (0)) * ff_v_swap_old_prefix) + (1))) /\ ((((exists ff_h_swap_old_prefix_terminal. ff_h_swap_old_prefix_terminal + S (r) = S ((S (n)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_terminal. ff_u_swap_old_prefix = ff_q_swap_old_prefix_terminal * S ((S (n)) * ff_v_swap_old_prefix) + (r))) /\ forall ff_i_swap_old_prefix. (exists ff_lt_swap_old_prefix_bound. ff_lt_swap_old_prefix_bound + S ff_i_swap_old_prefix = n) -> exists ff_p_swap_old_prefix ff_r_swap_old_prefix ff_s_swap_old_prefix. ((((exists ff_h_swap_old_prefix_factor. ff_h_swap_old_prefix_factor + S (ff_p_swap_old_prefix) = S ((S (ff_i_swap_old_prefix)) * c)) /\ exists ff_q_swap_old_prefix_factor. b = ff_q_swap_old_prefix_factor * S ((S (ff_i_swap_old_prefix)) * c) + (ff_p_swap_old_prefix))) /\ ((((exists ff_h_swap_old_prefix_partial. ff_h_swap_old_prefix_partial + S (ff_r_swap_old_prefix) = S ((S (ff_i_swap_old_prefix)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_partial. ff_u_swap_old_prefix = ff_q_swap_old_prefix_partial * S ((S (ff_i_swap_old_prefix)) * ff_v_swap_old_prefix) + (ff_r_swap_old_prefix))) /\ ((((exists ff_h_swap_old_prefix_successor. ff_h_swap_old_prefix_successor + S (ff_s_swap_old_prefix) = S ((S (S ff_i_swap_old_prefix)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_successor. ff_u_swap_old_prefix = ff_q_swap_old_prefix_successor * S ((S (S ff_i_swap_old_prefix)) * ff_v_swap_old_prefix) + (ff_s_swap_old_prefix))) /\ ff_s_swap_old_prefix = ff_r_swap_old_prefix * ff_p_swap_old_prefix)))))) /\ p = r * a)
  20. 0020specialize beta_product_succ_decompose b
  21. 0021specialize beta_product_succ_decompose c
  22. 0022specialize beta_product_succ_decompose n
  23. 0023specialize beta_product_succ_decompose p
  24. 0024apply beta_product_succ_decompose
  25. 0025exact hproduct_old
  26. 0026have hnew_decomp : ∃ a. ∃ r. BetaAt(z,d,n,a) ∧ (Product(z,d,n,r) ∧ q = r · a)
    Exact native replay linehave hnew_decomp : exists a r. (((exists ff_h_swap_new_last. ff_h_swap_new_last + S (a) = S ((S (n)) * d)) /\ exists ff_q_swap_new_last. z = ff_q_swap_new_last * S ((S (n)) * d) + (a))) /\ ((exists ff_u_swap_new_prefix ff_v_swap_new_prefix. ((((exists ff_h_swap_new_prefix_start. ff_h_swap_new_prefix_start + S (1) = S ((S (0)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_start. ff_u_swap_new_prefix = ff_q_swap_new_prefix_start * S ((S (0)) * ff_v_swap_new_prefix) + (1))) /\ ((((exists ff_h_swap_new_prefix_terminal. ff_h_swap_new_prefix_terminal + S (r) = S ((S (n)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_terminal. ff_u_swap_new_prefix = ff_q_swap_new_prefix_terminal * S ((S (n)) * ff_v_swap_new_prefix) + (r))) /\ forall ff_i_swap_new_prefix. (exists ff_lt_swap_new_prefix_bound. ff_lt_swap_new_prefix_bound + S ff_i_swap_new_prefix = n) -> exists ff_p_swap_new_prefix ff_r_swap_new_prefix ff_s_swap_new_prefix. ((((exists ff_h_swap_new_prefix_factor. ff_h_swap_new_prefix_factor + S (ff_p_swap_new_prefix) = S ((S (ff_i_swap_new_prefix)) * d)) /\ exists ff_q_swap_new_prefix_factor. z = ff_q_swap_new_prefix_factor * S ((S (ff_i_swap_new_prefix)) * d) + (ff_p_swap_new_prefix))) /\ ((((exists ff_h_swap_new_prefix_partial. ff_h_swap_new_prefix_partial + S (ff_r_swap_new_prefix) = S ((S (ff_i_swap_new_prefix)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_partial. ff_u_swap_new_prefix = ff_q_swap_new_prefix_partial * S ((S (ff_i_swap_new_prefix)) * ff_v_swap_new_prefix) + (ff_r_swap_new_prefix))) /\ ((((exists ff_h_swap_new_prefix_successor. ff_h_swap_new_prefix_successor + S (ff_s_swap_new_prefix) = S ((S (S ff_i_swap_new_prefix)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_successor. ff_u_swap_new_prefix = ff_q_swap_new_prefix_successor * S ((S (S ff_i_swap_new_prefix)) * ff_v_swap_new_prefix) + (ff_s_swap_new_prefix))) /\ ff_s_swap_new_prefix = ff_r_swap_new_prefix * ff_p_swap_new_prefix)))))) /\ q = r * a)
  27. 0027specialize beta_product_succ_decompose z
  28. 0028specialize beta_product_succ_decompose d
  29. 0029specialize beta_product_succ_decompose n
  30. 0030specialize beta_product_succ_decompose q
  31. 0031apply beta_product_succ_decompose
  32. 0032exact hproduct_new
  33. 0033cases hold_decomp
  34. 0034cases hold_decomp_witness
  35. 0035cases hold_decomp_witness_witness
  36. 0036cases hold_decomp_witness_witness_right
  37. 0037cases hnew_decomp
  38. 0038cases hnew_decomp_witness
  39. 0039cases hnew_decomp_witness_witness
  40. 0040cases hnew_decomp_witness_witness_right
  41. 0041have hold_last : x1 = y
  42. 0042specialize beta_at_unique b
  43. 0043specialize beta_at_unique c
  44. 0044specialize beta_at_unique n
  45. 0045specialize beta_at_unique x1
  46. 0046specialize beta_at_unique y
  47. 0047apply beta_at_unique
  48. 0048exact hold_decomp_witness_witness_left
  49. 0049exact hold_n
  50. 0050have hnew_last : x3 = x
  51. 0051specialize beta_at_unique z
  52. 0052specialize beta_at_unique d
  53. 0053specialize beta_at_unique n
  54. 0054specialize beta_at_unique x3
  55. 0055specialize beta_at_unique x
  56. 0056apply beta_at_unique
  57. 0057exact hnew_decomp_witness_witness_left
  58. 0058exact hnew_n
  59. 0059have hprefix_preserve : ∀ j. ∀ a. Lt(j,n) → ¬j = i → BetaAt(b,c,j,a) → BetaAt(z,d,j,a)
    Exact native replay linehave hprefix_preserve : forall j a. (exists h. h + S j = n) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists w. b = w * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists w. z = w * S ((S j) * d) + a)
  60. 0060intro j
  61. 0061intro a
  62. 0062intro hj
  63. 0063intro hji
  64. 0064intro hold
  65. 0065specialize hpreserve j
  66. 0066specialize hpreserve a
  67. 0067apply hpreserve
  68. 0068specialize le_succ (S j)
  69. 0069specialize le_succ n
  70. 0070apply le_succ
  71. 0071exact hj
  72. 0072exact hji
  73. 0073intro hjn
  74. 0074specialize lt_irrefl_expanded n
  75. 0075apply lt_irrefl_expanded
  76. 0076rewrite hjn at hj
  77. 0077exact hj
  78. 0078exact hold
  79. 0079have hbalance : x4 * x = x2 * y
  80. 0080specialize beta_product_replace_balance n
  81. 0081specialize beta_product_replace_balance b
  82. 0082specialize beta_product_replace_balance c
  83. 0083specialize beta_product_replace_balance z
  84. 0084specialize beta_product_replace_balance d
  85. 0085specialize beta_product_replace_balance i
  86. 0086specialize beta_product_replace_balance x
  87. 0087specialize beta_product_replace_balance y
  88. 0088specialize beta_product_replace_balance x2
  89. 0089specialize beta_product_replace_balance x4
  90. 0090apply beta_product_replace_balance
  91. 0091exact hi
  92. 0092exact hold_i
  93. 0093exact hnew_i
  94. 0094exact hprefix_preserve
  95. 0095exact hold_decomp_witness_witness_right_left
  96. 0096exact hnew_decomp_witness_witness_right_left
  97. 0097rewrite hold_decomp_witness_witness_right_right
  98. 0098rewrite hnew_decomp_witness_witness_right_right
  99. 0099rewrite hold_last
  100. 0100rewrite hnew_last
  101. 0101symm
  102. 0102exact hbalance