JT0032

jordan_canonical_crt_tuple_exists

Construct an actual tuple bounded by the product modulus with both prescribed residue tuples.

Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ m. ∀ n. ∀ b. ∀ c. ∀ d. ∀ e. ∀ k. ¬m = 0 → ¬n = 0 → Coprime(m,n) → ∃ x. ∃ y. JordanCanonicalTupleCRT(m,n,b,c,d,e,x,y,k)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixInto(b,c,l,B) · 1JordanTupleCongruence(n,b,c,d,e,k) · 3JordanTupleCRT(m,n,b,c,d,e,f,g,k) · 2JordanCanonicalTupleCRT(m,n,b,c,d,e,f,g,k) · 1Coprime(a,b) · 1

Actual proof prerequisites

jordan_crt_tuple_existsmul_ne_zero · checked external prerequisitejordan_tuple_normalize_existsjordan_tuple_congruence_divisormul_comm · checked external prerequisitejordan_tuple_congruence_transjordan_tuple_congruence_symmjordan_crt_tuple_leftjordan_crt_tuple_right
Original expanded first-order statement 
forall m n b c d e k. ~(m=0) -> ~(n=0) -> (forall jt_divisor_canonicalcrtcoprime. (exists jt_factor_canonicalcrtcoprimea. (m)=(jt_divisor_canonicalcrtcoprime)*jt_factor_canonicalcrtcoprimea) -> (exists jt_factor_canonicalcrtcoprimeb. (n)=(jt_divisor_canonicalcrtcoprime)*jt_factor_canonicalcrtcoprimeb) -> jt_divisor_canonicalcrtcoprime=1) -> exists f g. ((forall jt_index_canonicalcrtexistsbound. (exists jt_gap_canonicalcrtexistsboundindex. jt_gap_canonicalcrtexistsboundindex+S (jt_index_canonicalcrtexistsbound)=(k)) -> exists jt_value_canonicalcrtexistsbound. ((((exists fs_h_jt_canonicalcrtexistsboundat. fs_h_jt_canonicalcrtexistsboundat + S (jt_value_canonicalcrtexistsbound) = S ((S (jt_index_canonicalcrtexistsbound)) * g)) /\ exists fs_q_jt_canonicalcrtexistsboundat. f = fs_q_jt_canonicalcrtexistsboundat * S ((S (jt_index_canonicalcrtexistsbound)) * g) + (jt_value_canonicalcrtexistsbound))) /\ (exists jt_gap_canonicalcrtexistsboundvalue. jt_gap_canonicalcrtexistsboundvalue+S (jt_value_canonicalcrtexistsbound)=(m*n)))) /\ (((forall jt_index_canonicalcrtexistsleft jt_left_canonicalcrtexistsleft jt_right_canonicalcrtexistsleft. (exists jt_gap_canonicalcrtexistsleftindex. jt_gap_canonicalcrtexistsleftindex+S (jt_index_canonicalcrtexistsleft)=(k)) -> (((exists fs_h_jt_canonicalcrtexistsleftleft. fs_h_jt_canonicalcrtexistsleftleft + S (jt_left_canonicalcrtexistsleft) = S ((S (jt_index_canonicalcrtexistsleft)) * g)) /\ exists fs_q_jt_canonicalcrtexistsleftleft. f = fs_q_jt_canonicalcrtexistsleftleft * S ((S (jt_index_canonicalcrtexistsleft)) * g) + (jt_left_canonicalcrtexistsleft))) -> (((exists fs_h_jt_canonicalcrtexistsleftright. fs_h_jt_canonicalcrtexistsleftright + S (jt_right_canonicalcrtexistsleft) = S ((S (jt_index_canonicalcrtexistsleft)) * c)) /\ exists fs_q_jt_canonicalcrtexistsleftright. b = fs_q_jt_canonicalcrtexistsleftright * S ((S (jt_index_canonicalcrtexistsleft)) * c) + (jt_right_canonicalcrtexistsleft))) -> (exists jt_left_canonicalcrtexistsleftmod jt_right_canonicalcrtexistsleftmod. (jt_left_canonicalcrtexistsleft)+(m)*jt_left_canonicalcrtexistsleftmod=(jt_right_canonicalcrtexistsleft)+(m)*jt_right_canonicalcrtexistsleftmod)) /\ (forall jt_index_canonicalcrtexistsright jt_left_canonicalcrtexistsright jt_right_canonicalcrtexistsright. (exists jt_gap_canonicalcrtexistsrightindex. jt_gap_canonicalcrtexistsrightindex+S (jt_index_canonicalcrtexistsright)=(k)) -> (((exists fs_h_jt_canonicalcrtexistsrightleft. fs_h_jt_canonicalcrtexistsrightleft + S (jt_left_canonicalcrtexistsright) = S ((S (jt_index_canonicalcrtexistsright)) * g)) /\ exists fs_q_jt_canonicalcrtexistsrightleft. f = fs_q_jt_canonicalcrtexistsrightleft * S ((S (jt_index_canonicalcrtexistsright)) * g) + (jt_left_canonicalcrtexistsright))) -> (((exists fs_h_jt_canonicalcrtexistsrightright. fs_h_jt_canonicalcrtexistsrightright + S (jt_right_canonicalcrtexistsright) = S ((S (jt_index_canonicalcrtexistsright)) * e)) /\ exists fs_q_jt_canonicalcrtexistsrightright. d = fs_q_jt_canonicalcrtexistsrightright * S ((S (jt_index_canonicalcrtexistsright)) * e) + (jt_right_canonicalcrtexistsright))) -> (exists jt_left_canonicalcrtexistsrightmod jt_right_canonicalcrtexistsrightmod. (jt_left_canonicalcrtexistsright)+(n)*jt_left_canonicalcrtexistsrightmod=(jt_right_canonicalcrtexistsright)+(n)*jt_right_canonicalcrtexistsrightmod)))))

Complete tactic proof in conservative notation

All 131 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

131 script commands · 24 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 (7)
jordan crt tuple existsjordan tuple normalize existsjordan tuple congruence divisorjordan tuple congruence transjordan tuple congruence symmjordan crt tuple leftjordan crt tuple right
01Fix variables and assumptionsL1–10

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro k
  8. L8
    intro hm
  9. L9
    intro hn
  10. L10
    intro hcop
02Establish hfamilyL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan crt tuple exists.

  1. L11
    have hfamily : ∀ L. ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,L)Definitions: JordanTupleCRT(m,n,b,c,d,e,f,g,L)Original native command in the exact edition
  2. L12
    specialize jordan_crt_tuple_exists (m)
  3. L13
    specialize jordan_crt_tuple_exists (n)
  4. L14
    specialize jordan_crt_tuple_exists (b)
  5. L15
    specialize jordan_crt_tuple_exists (c)
  6. L16
    specialize jordan_crt_tuple_exists (d)
  7. L17
    specialize jordan_crt_tuple_exists (e)
  8. L18
    apply jordan_crt_tuple_exists
  9. L19
    exact hm
  10. L20
    exact hn
03Use earlier factsL21–21

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

  1. L21
    exact hcop
04Establish hrawL22–24

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

  1. L22
    have hraw : ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,k)Definitions: JordanTupleCRT(m,n,b,c,d,e,f,g,k)Original native command in the exact edition
  2. L23
    specialize hfamily (k)
  3. L24
    apply hfamily
05Separate the logical casesL25–26

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

  1. L25
    cases hraw
  2. L26
    cases hraw_witness
06Establish hproductL27–34

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

  1. L27
    have hproduct : ~(m*n=0)
  2. L28
    intro hz
  3. L29
    specialize mul_ne_zero (m)
  4. L30
    specialize mul_ne_zero (n)
  5. L31
    apply mul_ne_zero
  6. L32
    exact hm
  7. L33
    exact hn
  8. L34
    exact hz
07Establish hnormL35–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple normalize exists.

  1. L35
    have hnorm : ∃ u. ∃ v. BetaPrefixInto(u,v,k,m · n) ∧ JordanTupleCongruence(m · n,x,x1,u,v,k)Definitions: BetaPrefixInto(u,v,k,m · n)JordanTupleCongruence(m · n,x,x1,u,v,k)Original native command in the exact edition
  2. L36
    specialize jordan_tuple_normalize_exists (m*n)
  3. L37
    specialize jordan_tuple_normalize_exists (x)
  4. L38
    specialize jordan_tuple_normalize_exists (x1)
  5. L39
    specialize jordan_tuple_normalize_exists (k)
  6. L40
    apply jordan_tuple_normalize_exists
  7. L41
    exact hproduct
08Separate the logical casesL42–44

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

  1. L42
    cases hnorm
  2. L43
    cases hnorm_witness
  3. L44
    cases hnorm_witness_witness
09Construct an explicit witnessL45–46

Supply the displayed value, then prove that it has the required property.

  1. L45
    exists x2
  2. L46
    exists x3
10Separate the logical casesL47–47

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

  1. L47
    split
11Use earlier factsL48–48

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

  1. L48
    exact hnorm_witness_witness_left
12Separate the logical casesL49–49

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

  1. L49
    split
13Establish hsmallL50–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple congruence divisor.

  1. L50
    have hsmall : JordanTupleCongruence(m,x,x1,x2,x3,k)Definitions: JordanTupleCongruence(m,x,x1,x2,x3,k)Original native command in the exact edition
  2. L51
    specialize jordan_tuple_congruence_divisor (m)
  3. L52
    specialize jordan_tuple_congruence_divisor (m*n)
  4. L53
    specialize jordan_tuple_congruence_divisor (x)
  5. L54
    specialize jordan_tuple_congruence_divisor (x1)
  6. L55
    specialize jordan_tuple_congruence_divisor (x2)
  7. L56
    specialize jordan_tuple_congruence_divisor (x3)
  8. L57
    specialize jordan_tuple_congruence_divisor (k)
  9. L58
    apply jordan_tuple_congruence_divisor
14Construct an explicit witnessL59–59

Supply the displayed value, then prove that it has the required property.

  1. L59
    exists n
15Calculate and transport equalitiesL60–60

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

  1. L60
    refl
16Use earlier factsL61–70

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

  1. L61
    exact hnorm_witness_witness_right
  2. L62
    specialize jordan_tuple_congruence_trans (m)
  3. L63
    specialize jordan_tuple_congruence_trans (x2)
  4. L64
    specialize jordan_tuple_congruence_trans (x3)
  5. L65
    specialize jordan_tuple_congruence_trans (x)
  6. L66
    specialize jordan_tuple_congruence_trans (x1)
  7. L67
    specialize jordan_tuple_congruence_trans (b)
  8. L68
    specialize jordan_tuple_congruence_trans (c)
  9. L69
    specialize jordan_tuple_congruence_trans (k)
  10. L70
    apply jordan_tuple_congruence_trans
17Use earlier factsL71–80

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

  1. L71
    specialize jordan_tuple_congruence_symm (m)
  2. L72
    specialize jordan_tuple_congruence_symm (x)
  3. L73
    specialize jordan_tuple_congruence_symm (x1)
  4. L74
    specialize jordan_tuple_congruence_symm (x2)
  5. L75
    specialize jordan_tuple_congruence_symm (x3)
  6. L76
    specialize jordan_tuple_congruence_symm (k)
  7. L77
    apply jordan_tuple_congruence_symm
  8. L78
    exact hsmall
  9. L79
    specialize jordan_crt_tuple_left (m)
  10. L80
    specialize jordan_crt_tuple_left (n)
18Use earlier factsL81–89

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

  1. L81
    specialize jordan_crt_tuple_left (b)
  2. L82
    specialize jordan_crt_tuple_left (c)
  3. L83
    specialize jordan_crt_tuple_left (d)
  4. L84
    specialize jordan_crt_tuple_left (e)
  5. L85
    specialize jordan_crt_tuple_left (x)
  6. L86
    specialize jordan_crt_tuple_left (x1)
  7. L87
    specialize jordan_crt_tuple_left (k)
  8. L88
    apply jordan_crt_tuple_left
  9. L89
    exact hraw_witness_witness
19Establish hsmallL90–98

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple congruence divisor.

  1. L90
    have hsmall : JordanTupleCongruence(n,x,x1,x2,x3,k)Definitions: JordanTupleCongruence(n,x,x1,x2,x3,k)Original native command in the exact edition
  2. L91
    specialize jordan_tuple_congruence_divisor (n)
  3. L92
    specialize jordan_tuple_congruence_divisor (m*n)
  4. L93
    specialize jordan_tuple_congruence_divisor (x)
  5. L94
    specialize jordan_tuple_congruence_divisor (x1)
  6. L95
    specialize jordan_tuple_congruence_divisor (x2)
  7. L96
    specialize jordan_tuple_congruence_divisor (x3)
  8. L97
    specialize jordan_tuple_congruence_divisor (k)
  9. L98
    apply jordan_tuple_congruence_divisor
20Construct an explicit witnessL99–99

Supply the displayed value, then prove that it has the required property.

  1. L99
    exists m
21Use earlier factsL100–109

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

  1. L100
    specialize mul_comm (m)
  2. L101
    specialize mul_comm (n)
  3. L102
    apply mul_comm
  4. L103
    exact hnorm_witness_witness_right
  5. L104
    specialize jordan_tuple_congruence_trans (n)
  6. L105
    specialize jordan_tuple_congruence_trans (x2)
  7. L106
    specialize jordan_tuple_congruence_trans (x3)
  8. L107
    specialize jordan_tuple_congruence_trans (x)
  9. L108
    specialize jordan_tuple_congruence_trans (x1)
  10. L109
    specialize jordan_tuple_congruence_trans (d)
22Use earlier factsL110–119

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

  1. L110
    specialize jordan_tuple_congruence_trans (e)
  2. L111
    specialize jordan_tuple_congruence_trans (k)
  3. L112
    apply jordan_tuple_congruence_trans
  4. L113
    specialize jordan_tuple_congruence_symm (n)
  5. L114
    specialize jordan_tuple_congruence_symm (x)
  6. L115
    specialize jordan_tuple_congruence_symm (x1)
  7. L116
    specialize jordan_tuple_congruence_symm (x2)
  8. L117
    specialize jordan_tuple_congruence_symm (x3)
  9. L118
    specialize jordan_tuple_congruence_symm (k)
  10. L119
    apply jordan_tuple_congruence_symm
23Use earlier factsL120–129

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

  1. L120
    exact hsmall
  2. L121
    specialize jordan_crt_tuple_right (m)
  3. L122
    specialize jordan_crt_tuple_right (n)
  4. L123
    specialize jordan_crt_tuple_right (b)
  5. L124
    specialize jordan_crt_tuple_right (c)
  6. L125
    specialize jordan_crt_tuple_right (d)
  7. L126
    specialize jordan_crt_tuple_right (e)
  8. L127
    specialize jordan_crt_tuple_right (x)
  9. L128
    specialize jordan_crt_tuple_right (x1)
  10. L129
    specialize jordan_crt_tuple_right (k)
24Use earlier factsL130–131

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

  1. L130
    apply jordan_crt_tuple_right
  2. L131
    exact hraw_witness_witness

Library-wide reading audit

Original defined command ledger · 131 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro k
  8. 0008intro hm
  9. 0009intro hn
  10. 0010intro hcop
  11. 0011have hfamily : ∀ L. ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,L)
  12. 0012specialize jordan_crt_tuple_exists (m)
  13. 0013specialize jordan_crt_tuple_exists (n)
  14. 0014specialize jordan_crt_tuple_exists (b)
  15. 0015specialize jordan_crt_tuple_exists (c)
  16. 0016specialize jordan_crt_tuple_exists (d)
  17. 0017specialize jordan_crt_tuple_exists (e)
  18. 0018apply jordan_crt_tuple_exists
  19. 0019exact hm
  20. 0020exact hn
  21. 0021exact hcop
  22. 0022have hraw : ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,k)
  23. 0023specialize hfamily (k)
  24. 0024apply hfamily
  25. 0025cases hraw
  26. 0026cases hraw_witness
  27. 0027have hproduct : ~(m*n=0)
  28. 0028intro hz
  29. 0029specialize mul_ne_zero (m)
  30. 0030specialize mul_ne_zero (n)
  31. 0031apply mul_ne_zero
  32. 0032exact hm
  33. 0033exact hn
  34. 0034exact hz
  35. 0035have hnorm : ∃ u. ∃ v. BetaPrefixInto(u,v,k,m · n) ∧ JordanTupleCongruence(m · n,x,x1,u,v,k)
  36. 0036specialize jordan_tuple_normalize_exists (m*n)
  37. 0037specialize jordan_tuple_normalize_exists (x)
  38. 0038specialize jordan_tuple_normalize_exists (x1)
  39. 0039specialize jordan_tuple_normalize_exists (k)
  40. 0040apply jordan_tuple_normalize_exists
  41. 0041exact hproduct
  42. 0042cases hnorm
  43. 0043cases hnorm_witness
  44. 0044cases hnorm_witness_witness
  45. 0045exists x2
  46. 0046exists x3
  47. 0047split
  48. 0048exact hnorm_witness_witness_left
  49. 0049split
  50. 0050have hsmall : JordanTupleCongruence(m,x,x1,x2,x3,k)
  51. 0051specialize jordan_tuple_congruence_divisor (m)
  52. 0052specialize jordan_tuple_congruence_divisor (m*n)
  53. 0053specialize jordan_tuple_congruence_divisor (x)
  54. 0054specialize jordan_tuple_congruence_divisor (x1)
  55. 0055specialize jordan_tuple_congruence_divisor (x2)
  56. 0056specialize jordan_tuple_congruence_divisor (x3)
  57. 0057specialize jordan_tuple_congruence_divisor (k)
  58. 0058apply jordan_tuple_congruence_divisor
  59. 0059exists n
  60. 0060refl
  61. 0061exact hnorm_witness_witness_right
  62. 0062specialize jordan_tuple_congruence_trans (m)
  63. 0063specialize jordan_tuple_congruence_trans (x2)
  64. 0064specialize jordan_tuple_congruence_trans (x3)
  65. 0065specialize jordan_tuple_congruence_trans (x)
  66. 0066specialize jordan_tuple_congruence_trans (x1)
  67. 0067specialize jordan_tuple_congruence_trans (b)
  68. 0068specialize jordan_tuple_congruence_trans (c)
  69. 0069specialize jordan_tuple_congruence_trans (k)
  70. 0070apply jordan_tuple_congruence_trans
  71. 0071specialize jordan_tuple_congruence_symm (m)
  72. 0072specialize jordan_tuple_congruence_symm (x)
  73. 0073specialize jordan_tuple_congruence_symm (x1)
  74. 0074specialize jordan_tuple_congruence_symm (x2)
  75. 0075specialize jordan_tuple_congruence_symm (x3)
  76. 0076specialize jordan_tuple_congruence_symm (k)
  77. 0077apply jordan_tuple_congruence_symm
  78. 0078exact hsmall
  79. 0079specialize jordan_crt_tuple_left (m)
  80. 0080specialize jordan_crt_tuple_left (n)
  81. 0081specialize jordan_crt_tuple_left (b)
  82. 0082specialize jordan_crt_tuple_left (c)
  83. 0083specialize jordan_crt_tuple_left (d)
  84. 0084specialize jordan_crt_tuple_left (e)
  85. 0085specialize jordan_crt_tuple_left (x)
  86. 0086specialize jordan_crt_tuple_left (x1)
  87. 0087specialize jordan_crt_tuple_left (k)
  88. 0088apply jordan_crt_tuple_left
  89. 0089exact hraw_witness_witness
  90. 0090have hsmall : JordanTupleCongruence(n,x,x1,x2,x3,k)
  91. 0091specialize jordan_tuple_congruence_divisor (n)
  92. 0092specialize jordan_tuple_congruence_divisor (m*n)
  93. 0093specialize jordan_tuple_congruence_divisor (x)
  94. 0094specialize jordan_tuple_congruence_divisor (x1)
  95. 0095specialize jordan_tuple_congruence_divisor (x2)
  96. 0096specialize jordan_tuple_congruence_divisor (x3)
  97. 0097specialize jordan_tuple_congruence_divisor (k)
  98. 0098apply jordan_tuple_congruence_divisor
  99. 0099exists m
  100. 0100specialize mul_comm (m)
  101. 0101specialize mul_comm (n)
  102. 0102apply mul_comm
  103. 0103exact hnorm_witness_witness_right
  104. 0104specialize jordan_tuple_congruence_trans (n)
  105. 0105specialize jordan_tuple_congruence_trans (x2)
  106. 0106specialize jordan_tuple_congruence_trans (x3)
  107. 0107specialize jordan_tuple_congruence_trans (x)
  108. 0108specialize jordan_tuple_congruence_trans (x1)
  109. 0109specialize jordan_tuple_congruence_trans (d)
  110. 0110specialize jordan_tuple_congruence_trans (e)
  111. 0111specialize jordan_tuple_congruence_trans (k)
  112. 0112apply jordan_tuple_congruence_trans
  113. 0113specialize jordan_tuple_congruence_symm (n)
  114. 0114specialize jordan_tuple_congruence_symm (x)
  115. 0115specialize jordan_tuple_congruence_symm (x1)
  116. 0116specialize jordan_tuple_congruence_symm (x2)
  117. 0117specialize jordan_tuple_congruence_symm (x3)
  118. 0118specialize jordan_tuple_congruence_symm (k)
  119. 0119apply jordan_tuple_congruence_symm
  120. 0120exact hsmall
  121. 0121specialize jordan_crt_tuple_right (m)
  122. 0122specialize jordan_crt_tuple_right (n)
  123. 0123specialize jordan_crt_tuple_right (b)
  124. 0124specialize jordan_crt_tuple_right (c)
  125. 0125specialize jordan_crt_tuple_right (d)
  126. 0126specialize jordan_crt_tuple_right (e)
  127. 0127specialize jordan_crt_tuple_right (x)
  128. 0128specialize jordan_crt_tuple_right (x1)
  129. 0129specialize jordan_crt_tuple_right (k)
  130. 0130apply jordan_crt_tuple_right
  131. 0131exact hraw_witness_witness