PA00B7 · theorem

paired_successor_lift_adjacent_units

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

Successor-lifted adjacent inverse indices multiply to one modulo p.

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. ∀ n. ∀ u. ∀ v. ∀ b. ∀ c. ∀ f. ∀ g. ∀ m. InversePrefix(p,n,u,v,n) → (∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → (∀ x. Lt(x,m) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,z))) → (∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)) → ∀ x. ∀ y. ∀ z. Lt(x,m) → BetaAt(f,g,x + x,y) → BetaAt(f,g,S (x + x),z) → BalancedInverse(p,y,z)

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 PD0031 BalancedInverse PD0037 InversePrefix

15 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0036 InverseIndex

12 occurrences

Exact expanded native-PA statement
forall p n u v b c f g m. (forall wip_index_wsl_inverse. (exists wip_gap_wsl_inverse_prefix_bound. wip_gap_wsl_inverse_prefix_bound + S wip_index_wsl_inverse = n) -> exists wip_mate_wsl_inverse. ((((exists wip_beta_height_wsl_inverse_decoded. wip_beta_height_wsl_inverse_decoded + S (wip_mate_wsl_inverse) = S ((S (wip_index_wsl_inverse)) * v)) /\ exists wip_beta_quotient_wsl_inverse_decoded. u = wip_beta_quotient_wsl_inverse_decoded * S ((S (wip_index_wsl_inverse)) * v) + (wip_mate_wsl_inverse))) /\ ((exists wip_gap_wsl_inverse_inverse_index_bound. wip_gap_wsl_inverse_inverse_index_bound + S wip_index_wsl_inverse = n) /\ ((exists wip_gap_wsl_inverse_inverse_mate_bound. wip_gap_wsl_inverse_inverse_mate_bound + S wip_mate_wsl_inverse = n) /\ (exists wip_mod_left_wsl_inverse_inverse_mod wip_mod_right_wsl_inverse_inverse_mod. ((S wip_index_wsl_inverse) * S wip_mate_wsl_inverse) + p * wip_mod_left_wsl_inverse_inverse_mod = 1 + p * wip_mod_right_wsl_inverse_inverse_mod))))) -> (forall fom_index_wsl_bounded. (exists fom_gap_wsl_bounded_index_bound. fom_gap_wsl_bounded_index_bound + S (fom_index_wsl_bounded) = m + m) -> exists fom_value_wsl_bounded. ((((exists fom_beta_height_wsl_bounded_entry. fom_beta_height_wsl_bounded_entry + S (fom_value_wsl_bounded) = S ((S (fom_index_wsl_bounded)) * c)) /\ exists fom_beta_quotient_wsl_bounded_entry. b = fom_beta_quotient_wsl_bounded_entry * S ((S (fom_index_wsl_bounded)) * c) + (fom_value_wsl_bounded))) /\ (exists fom_gap_wsl_bounded_value_bound. fom_gap_wsl_bounded_value_bound + S (fom_value_wsl_bounded) = n))) -> (forall wpop_pair_wsl_pairs. (exists wpo_gap_wsl_pairs_pair_bound. wpo_gap_wsl_pairs_pair_bound + S (wpop_pair_wsl_pairs) = m) -> exists wpop_left_wsl_pairs wpop_right_wsl_pairs. ((((exists wpo_beta_height_wsl_pairs_left_entry. wpo_beta_height_wsl_pairs_left_entry + S (wpop_left_wsl_pairs) = S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c)) /\ exists wpo_beta_quotient_wsl_pairs_left_entry. b = wpo_beta_quotient_wsl_pairs_left_entry * S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c) + (wpop_left_wsl_pairs))) /\ ((((exists wpo_beta_height_wsl_pairs_right_entry. wpo_beta_height_wsl_pairs_right_entry + S (wpop_right_wsl_pairs) = S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c)) /\ exists wpo_beta_quotient_wsl_pairs_right_entry. b = wpo_beta_quotient_wsl_pairs_right_entry * S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c) + (wpop_right_wsl_pairs))) /\ (((exists wpo_beta_height_wsl_pairs_inverse_entry. wpo_beta_height_wsl_pairs_inverse_entry + S (wpop_right_wsl_pairs) = S ((S (wpop_left_wsl_pairs)) * v)) /\ exists wpo_beta_quotient_wsl_pairs_inverse_entry. u = wpo_beta_quotient_wsl_pairs_inverse_entry * S ((S (wpop_left_wsl_pairs)) * v) + (wpop_right_wsl_pairs)))))) -> (forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) -> (forall wpp_pair_wsl_adjacent wpp_left_wsl_adjacent wpp_right_wsl_adjacent. (exists wpp_gap_wsl_adjacent_pair_bound. wpp_gap_wsl_adjacent_pair_bound + S (wpp_pair_wsl_adjacent) = m) -> (((exists wpp_beta_height_wsl_adjacent_left_entry. wpp_beta_height_wsl_adjacent_left_entry + S (wpp_left_wsl_adjacent) = S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_left_entry. f = wpp_beta_quotient_wsl_adjacent_left_entry * S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_left_wsl_adjacent))) -> (((exists wpp_beta_height_wsl_adjacent_right_entry. wpp_beta_height_wsl_adjacent_right_entry + S (wpp_right_wsl_adjacent) = S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_right_entry. f = wpp_beta_quotient_wsl_adjacent_right_entry * S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_right_wsl_adjacent))) -> (exists wpp_mod_left_wsl_adjacent_pair_mod wpp_mod_right_wsl_adjacent_pair_mod. (wpp_left_wsl_adjacent * wpp_right_wsl_adjacent) + p * wpp_mod_left_wsl_adjacent_pair_mod = (1) + p * wpp_mod_right_wsl_adjacent_pair_mod))

Proof neighborhood

Direct theorem prerequisites

PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA002F beta_at_unique

Direct theorem dependents

PA00B8 paired_pair_order_factor_code_exists

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

106 script commands · 19 reading checkpoints · 12 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 (3)
pair index left below doublepair index right below doublebeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro m
  10. L10
    intro hinverse
02Fix variables and assumptionsL11–19

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

  1. L11
    intro hbounded
  2. L12
    intro hpairs
  3. L13
    intro hlift
  4. L14
    intro t
  5. L15
    intro a
  6. L16
    intro d
  7. L17
    intro ht
  8. L18
    intro ha
  9. L19
    intro hd
03Establish hpairL20–23

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

  1. L20
    have hpair : ∃ i. ∃ j. BetaAt(b,c,t + t,i) ∧ (BetaAt(b,c,S (t + t),j) ∧ BetaAt(u,v,i,j))Definitions: BetaAt(b,c,t + t,i)BetaAt(b,c,S (t + t),j)BetaAt(u,v,i,j)Original native command in the exact edition
  2. L21
    specialize hpairs t
  3. L22
    apply hpairs
  4. L23
    exact ht
04Separate the logical casesL24–27

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

  1. L24
    cases hpair
  2. L25
    cases hpair_witness
  3. L26
    cases hpair_witness_witness
  4. L27
    cases hpair_witness_witness_right
05Establish hevenL28–32

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

  1. L28
    have heven : Lt(t + t,m + m)Definitions: Lt(t + t,m + m)Original native command in the exact edition
  2. L29
    specialize pair_index_left_below_double t
  3. L30
    specialize pair_index_left_below_double m
  4. L31
    apply pair_index_left_below_double
  5. L32
    exact ht
06Establish hoddL33–37

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

  1. L33
    have hodd : Lt(S (t + t),m + m)Definitions: Lt(S (t + t),m + m)Original native command in the exact edition
  2. L34
    specialize pair_index_right_below_double t
  3. L35
    specialize pair_index_right_below_double m
  4. L36
    apply pair_index_right_below_double
  5. L37
    exact ht
07Establish hlift_leftL38–43

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

  1. L38
    have hlift_left : BetaAt(f,g,t + t,S x)Definitions: BetaAt(f,g,t + t,S x)Original native command in the exact edition
  2. L39
    specialize hlift (t + t)
  3. L40
    specialize hlift x
  4. L41
    apply hlift
  5. L42
    exact heven
  6. L43
    exact hpair_witness_witness_left
08Establish hlift_rightL44–49

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

  1. L44
    have hlift_right : BetaAt(f,g,S (t + t),S x1)Definitions: BetaAt(f,g,S (t + t),S x1)Original native command in the exact edition
  2. L45
    specialize hlift (S (t + t))
  3. L46
    specialize hlift x1
  4. L47
    apply hlift
  5. L48
    exact hodd
  6. L49
    exact hpair_witness_witness_right_left
09Establish haeqL50–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 haeq : a = S x
  2. L51
    specialize beta_at_unique f
  3. L52
    specialize beta_at_unique g
  4. L53
    specialize beta_at_unique (t + t)
  5. L54
    specialize beta_at_unique a
  6. L55
    specialize beta_at_unique (S x)
  7. L56
    apply beta_at_unique
  8. L57
    exact ha
  9. L58
    exact hlift_left
10Establish hdeqL59–67

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

  1. L59
    have hdeq : d = S x1
  2. L60
    specialize beta_at_unique f
  3. L61
    specialize beta_at_unique g
  4. L62
    specialize beta_at_unique (S (t + t))
  5. L63
    specialize beta_at_unique d
  6. L64
    specialize beta_at_unique (S x1)
  7. L65
    apply beta_at_unique
  8. L66
    exact hd
  9. L67
    exact hlift_right
11Establish hbounded_dataL68–71

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

  1. L68
    have hbounded_data : ∃ w. BetaAt(b,c,t + t,w) ∧ Lt(w,n)Definitions: BetaAt(b,c,t + t,w)Lt(w,n)Original native command in the exact edition
  2. L69
    specialize hbounded (t + t)
  3. L70
    apply hbounded
  4. L71
    exact heven
12Separate the logical casesL72–73

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

  1. L72
    cases hbounded_data
  2. L73
    cases hbounded_data_witness
13Establish hieqL74–82

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

  1. L74
    have hieq : x = x2
  2. L75
    specialize beta_at_unique b
  3. L76
    specialize beta_at_unique c
  4. L77
    specialize beta_at_unique (t + t)
  5. L78
    specialize beta_at_unique x
  6. L79
    specialize beta_at_unique x2
  7. L80
    apply beta_at_unique
  8. L81
    exact hpair_witness_witness_left
  9. L82
    exact hbounded_data_witness_left
14Establish hiboundL83–85

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

  1. L83
    have hibound : Lt(x,n)Definitions: Lt(x,n)Original native command in the exact edition
  2. L84
    rewrite hieq
  3. L85
    exact hbounded_data_witness_right
15Establish hinverse_dataL86–89

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

  1. L86
    have hinverse_data : ∃ q. BetaAt(u,v,x,q) ∧ InverseIndex(p,n,x,q)Definitions: BetaAt(u,v,x,q)InverseIndex(p,n,x,q)Original native command in the exact edition
  2. L87
    specialize hinverse x
  3. L88
    apply hinverse
  4. L89
    exact hibound
16Separate the logical casesL90–93

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

  1. L90
    cases hinverse_data
  2. L91
    cases hinverse_data_witness
  3. L92
    cases hinverse_data_witness_right
  4. L93
    cases hinverse_data_witness_right_right
17Establish hjeqL94–103

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

  1. L94
    have hjeq : x1 = x3
  2. L95
    specialize beta_at_unique u
  3. L96
    specialize beta_at_unique v
  4. L97
    specialize beta_at_unique x
  5. L98
    specialize beta_at_unique x1
  6. L99
    specialize beta_at_unique x3
  7. L100
    apply beta_at_unique
  8. L101
    exact hpair_witness_witness_right_right
  9. L102
    exact hinverse_data_witness_left
  10. L103
    rewrite haeq
18Calculate and transport equalitiesL104–105

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

  1. L104
    rewrite hdeq
  2. L105
    rewrite hjeq
19Use earlier factsL106–106

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

  1. L106
    exact hinverse_data_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 106 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro f
  8. 0008intro g
  9. 0009intro m
  10. 0010intro hinverse
  11. 0011intro hbounded
  12. 0012intro hpairs
  13. 0013intro hlift
  14. 0014intro t
  15. 0015intro a
  16. 0016intro d
  17. 0017intro ht
  18. 0018intro ha
  19. 0019intro hd
  20. 0020have hpair : ∃ i. ∃ j. BetaAt(b,c,t + t,i) ∧ (BetaAt(b,c,S (t + t),j) ∧ BetaAt(u,v,i,j))
    Exact native replay linehave hpair : exists i j. ((((exists wpo_beta_height_wsl_order_even_i. wpo_beta_height_wsl_order_even_i + S (i) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_wsl_order_even_i. b = wpo_beta_quotient_wsl_order_even_i * S ((S (t + t)) * c) + (i))) /\ ((((exists wpo_beta_height_wsl_order_odd_j. wpo_beta_height_wsl_order_odd_j + S (j) = S ((S (S (t + t))) * c)) /\ exists wpo_beta_quotient_wsl_order_odd_j. b = wpo_beta_quotient_wsl_order_odd_j * S ((S (S (t + t))) * c) + (j))) /\ (((exists wpo_beta_height_wsl_inverse_i_j. wpo_beta_height_wsl_inverse_i_j + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wsl_inverse_i_j. u = wpo_beta_quotient_wsl_inverse_i_j * S ((S (i)) * v) + (j)))))
  21. 0021specialize hpairs t
  22. 0022apply hpairs
  23. 0023exact ht
  24. 0024cases hpair
  25. 0025cases hpair_witness
  26. 0026cases hpair_witness_witness
  27. 0027cases hpair_witness_witness_right
  28. 0028have heven : Lt(t + t,m + m)
    Exact native replay linehave heven : exists wpo_gap_wsl_even_bound. wpo_gap_wsl_even_bound + S (t + t) = m + m
  29. 0029specialize pair_index_left_below_double t
  30. 0030specialize pair_index_left_below_double m
  31. 0031apply pair_index_left_below_double
  32. 0032exact ht
  33. 0033have hodd : Lt(S (t + t),m + m)
    Exact native replay linehave hodd : exists wpo_gap_wsl_odd_bound. wpo_gap_wsl_odd_bound + S (S (t + t)) = m + m
  34. 0034specialize pair_index_right_below_double t
  35. 0035specialize pair_index_right_below_double m
  36. 0036apply pair_index_right_below_double
  37. 0037exact ht
  38. 0038have hlift_left : BetaAt(f,g,t + t,S x)
    Exact native replay linehave hlift_left : ((exists wpo_beta_height_wsl_lifted_even_i. wpo_beta_height_wsl_lifted_even_i + S (S x) = S ((S (t + t)) * g)) /\ exists wpo_beta_quotient_wsl_lifted_even_i. f = wpo_beta_quotient_wsl_lifted_even_i * S ((S (t + t)) * g) + (S x))
  39. 0039specialize hlift (t + t)
  40. 0040specialize hlift x
  41. 0041apply hlift
  42. 0042exact heven
  43. 0043exact hpair_witness_witness_left
  44. 0044have hlift_right : BetaAt(f,g,S (t + t),S x1)
    Exact native replay linehave hlift_right : ((exists wpo_beta_height_wsl_lifted_odd_j. wpo_beta_height_wsl_lifted_odd_j + S (S x1) = S ((S (S (t + t))) * g)) /\ exists wpo_beta_quotient_wsl_lifted_odd_j. f = wpo_beta_quotient_wsl_lifted_odd_j * S ((S (S (t + t))) * g) + (S x1))
  45. 0045specialize hlift (S (t + t))
  46. 0046specialize hlift x1
  47. 0047apply hlift
  48. 0048exact hodd
  49. 0049exact hpair_witness_witness_right_left
  50. 0050have haeq : a = S x
  51. 0051specialize beta_at_unique f
  52. 0052specialize beta_at_unique g
  53. 0053specialize beta_at_unique (t + t)
  54. 0054specialize beta_at_unique a
  55. 0055specialize beta_at_unique (S x)
  56. 0056apply beta_at_unique
  57. 0057exact ha
  58. 0058exact hlift_left
  59. 0059have hdeq : d = S x1
  60. 0060specialize beta_at_unique f
  61. 0061specialize beta_at_unique g
  62. 0062specialize beta_at_unique (S (t + t))
  63. 0063specialize beta_at_unique d
  64. 0064specialize beta_at_unique (S x1)
  65. 0065apply beta_at_unique
  66. 0066exact hd
  67. 0067exact hlift_right
  68. 0068have hbounded_data : ∃ w. BetaAt(b,c,t + t,w) ∧ Lt(w,n)
    Exact native replay linehave hbounded_data : exists w. ((((exists wpo_beta_height_wsl_bounded_even_entry. wpo_beta_height_wsl_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_wsl_bounded_even_entry. b = wpo_beta_quotient_wsl_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_wsl_bounded_even_value. wpo_gap_wsl_bounded_even_value + S (w) = n))
  69. 0069specialize hbounded (t + t)
  70. 0070apply hbounded
  71. 0071exact heven
  72. 0072cases hbounded_data
  73. 0073cases hbounded_data_witness
  74. 0074have hieq : x = x2
  75. 0075specialize beta_at_unique b
  76. 0076specialize beta_at_unique c
  77. 0077specialize beta_at_unique (t + t)
  78. 0078specialize beta_at_unique x
  79. 0079specialize beta_at_unique x2
  80. 0080apply beta_at_unique
  81. 0081exact hpair_witness_witness_left
  82. 0082exact hbounded_data_witness_left
  83. 0083have hibound : Lt(x,n)
    Exact native replay linehave hibound : exists h. h + S x = n
  84. 0084rewrite hieq
  85. 0085exact hbounded_data_witness_right
  86. 0086have hinverse_data : ∃ q. BetaAt(u,v,x,q) ∧ InverseIndex(p,n,x,q)
    Exact native replay linehave hinverse_data : exists q. ((((exists wpo_beta_height_wsl_inverse_at_i_entry. wpo_beta_height_wsl_inverse_at_i_entry + S (q) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_wsl_inverse_at_i_entry. u = wpo_beta_quotient_wsl_inverse_at_i_entry * S ((S (x)) * v) + (q))) /\ ((exists wpo_gap_wsl_inverse_at_i_source_bound. wpo_gap_wsl_inverse_at_i_source_bound + S (x) = n) /\ ((exists wpo_gap_wsl_inverse_at_i_mate_bound. wpo_gap_wsl_inverse_at_i_mate_bound + S (q) = n) /\ exists y z. (S x * S q) + p * y = 1 + p * z)))
  87. 0087specialize hinverse x
  88. 0088apply hinverse
  89. 0089exact hibound
  90. 0090cases hinverse_data
  91. 0091cases hinverse_data_witness
  92. 0092cases hinverse_data_witness_right
  93. 0093cases hinverse_data_witness_right_right
  94. 0094have hjeq : x1 = x3
  95. 0095specialize beta_at_unique u
  96. 0096specialize beta_at_unique v
  97. 0097specialize beta_at_unique x
  98. 0098specialize beta_at_unique x1
  99. 0099specialize beta_at_unique x3
  100. 0100apply beta_at_unique
  101. 0101exact hpair_witness_witness_right_right
  102. 0102exact hinverse_data_witness_left
  103. 0103rewrite haeq
  104. 0104rewrite hdeq
  105. 0105rewrite hjeq
  106. 0106exact hinverse_data_witness_right_right_right