PA007N

beta_product_pointwise_mul_exact

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

Pointwise products of synchronized beta prefixes multiply their exact finite products.

Exact expanded PA statement

forall mb mc sb sc tb tc l M Sprod T. (forall fpmp_index_product_alignment fpmp_left_product_alignment fpmp_right_product_alignment fpmp_target_product_alignment. (exists fpmp_gap_product_alignment. fpmp_gap_product_alignment + S fpmp_index_product_alignment = l) -> (((exists ff_h_fpmp_product_alignment_left. ff_h_fpmp_product_alignment_left + S (fpmp_left_product_alignment) = S ((S (fpmp_index_product_alignment)) * mc)) /\ exists ff_q_fpmp_product_alignment_left. mb = ff_q_fpmp_product_alignment_left * S ((S (fpmp_index_product_alignment)) * mc) + (fpmp_left_product_alignment))) -> (((exists ff_h_fpmp_product_alignment_right. ff_h_fpmp_product_alignment_right + S (fpmp_right_product_alignment) = S ((S (fpmp_index_product_alignment)) * sc)) /\ exists ff_q_fpmp_product_alignment_right. sb = ff_q_fpmp_product_alignment_right * S ((S (fpmp_index_product_alignment)) * sc) + (fpmp_right_product_alignment))) -> (((exists ff_h_fpmp_product_alignment_target. ff_h_fpmp_product_alignment_target + S (fpmp_target_product_alignment) = S ((S (fpmp_index_product_alignment)) * tc)) /\ exists ff_q_fpmp_product_alignment_target. tb = ff_q_fpmp_product_alignment_target * S ((S (fpmp_index_product_alignment)) * tc) + (fpmp_target_product_alignment))) -> fpmp_target_product_alignment = fpmp_left_product_alignment * fpmp_right_product_alignment) -> (exists ff_u_product_left ff_v_product_left. ((((exists ff_h_product_left_start. ff_h_product_left_start + S (1) = S ((S (0)) * ff_v_product_left)) /\ exists ff_q_product_left_start. ff_u_product_left = ff_q_product_left_start * S ((S (0)) * ff_v_product_left) + (1))) /\ ((((exists ff_h_product_left_terminal. ff_h_product_left_terminal + S (M) = S ((S (l)) * ff_v_product_left)) /\ exists ff_q_product_left_terminal. ff_u_product_left = ff_q_product_left_terminal * S ((S (l)) * ff_v_product_left) + (M))) /\ forall ff_i_product_left. (exists ff_lt_product_left_bound. ff_lt_product_left_bound + S ff_i_product_left = l) -> exists ff_p_product_left ff_r_product_left ff_s_product_left. ((((exists ff_h_product_left_factor. ff_h_product_left_factor + S (ff_p_product_left) = S ((S (ff_i_product_left)) * mc)) /\ exists ff_q_product_left_factor. mb = ff_q_product_left_factor * S ((S (ff_i_product_left)) * mc) + (ff_p_product_left))) /\ ((((exists ff_h_product_left_partial. ff_h_product_left_partial + S (ff_r_product_left) = S ((S (ff_i_product_left)) * ff_v_product_left)) /\ exists ff_q_product_left_partial. ff_u_product_left = ff_q_product_left_partial * S ((S (ff_i_product_left)) * ff_v_product_left) + (ff_r_product_left))) /\ ((((exists ff_h_product_left_successor. ff_h_product_left_successor + S (ff_s_product_left) = S ((S (S ff_i_product_left)) * ff_v_product_left)) /\ exists ff_q_product_left_successor. ff_u_product_left = ff_q_product_left_successor * S ((S (S ff_i_product_left)) * ff_v_product_left) + (ff_s_product_left))) /\ ff_s_product_left = ff_r_product_left * ff_p_product_left)))))) -> (exists ff_u_product_right ff_v_product_right. ((((exists ff_h_product_right_start. ff_h_product_right_start + S (1) = S ((S (0)) * ff_v_product_right)) /\ exists ff_q_product_right_start. ff_u_product_right = ff_q_product_right_start * S ((S (0)) * ff_v_product_right) + (1))) /\ ((((exists ff_h_product_right_terminal. ff_h_product_right_terminal + S (Sprod) = S ((S (l)) * ff_v_product_right)) /\ exists ff_q_product_right_terminal. ff_u_product_right = ff_q_product_right_terminal * S ((S (l)) * ff_v_product_right) + (Sprod))) /\ forall ff_i_product_right. (exists ff_lt_product_right_bound. ff_lt_product_right_bound + S ff_i_product_right = l) -> exists ff_p_product_right ff_r_product_right ff_s_product_right. ((((exists ff_h_product_right_factor. ff_h_product_right_factor + S (ff_p_product_right) = S ((S (ff_i_product_right)) * sc)) /\ exists ff_q_product_right_factor. sb = ff_q_product_right_factor * S ((S (ff_i_product_right)) * sc) + (ff_p_product_right))) /\ ((((exists ff_h_product_right_partial. ff_h_product_right_partial + S (ff_r_product_right) = S ((S (ff_i_product_right)) * ff_v_product_right)) /\ exists ff_q_product_right_partial. ff_u_product_right = ff_q_product_right_partial * S ((S (ff_i_product_right)) * ff_v_product_right) + (ff_r_product_right))) /\ ((((exists ff_h_product_right_successor. ff_h_product_right_successor + S (ff_s_product_right) = S ((S (S ff_i_product_right)) * ff_v_product_right)) /\ exists ff_q_product_right_successor. ff_u_product_right = ff_q_product_right_successor * S ((S (S ff_i_product_right)) * ff_v_product_right) + (ff_s_product_right))) /\ ff_s_product_right = ff_r_product_right * ff_p_product_right)))))) -> (exists ff_u_product_target ff_v_product_target. ((((exists ff_h_product_target_start. ff_h_product_target_start + S (1) = S ((S (0)) * ff_v_product_target)) /\ exists ff_q_product_target_start. ff_u_product_target = ff_q_product_target_start * S ((S (0)) * ff_v_product_target) + (1))) /\ ((((exists ff_h_product_target_terminal. ff_h_product_target_terminal + S (T) = S ((S (l)) * ff_v_product_target)) /\ exists ff_q_product_target_terminal. ff_u_product_target = ff_q_product_target_terminal * S ((S (l)) * ff_v_product_target) + (T))) /\ forall ff_i_product_target. (exists ff_lt_product_target_bound. ff_lt_product_target_bound + S ff_i_product_target = l) -> exists ff_p_product_target ff_r_product_target ff_s_product_target. ((((exists ff_h_product_target_factor. ff_h_product_target_factor + S (ff_p_product_target) = S ((S (ff_i_product_target)) * tc)) /\ exists ff_q_product_target_factor. tb = ff_q_product_target_factor * S ((S (ff_i_product_target)) * tc) + (ff_p_product_target))) /\ ((((exists ff_h_product_target_partial. ff_h_product_target_partial + S (ff_r_product_target) = S ((S (ff_i_product_target)) * ff_v_product_target)) /\ exists ff_q_product_target_partial. ff_u_product_target = ff_q_product_target_partial * S ((S (ff_i_product_target)) * ff_v_product_target) + (ff_r_product_target))) /\ ((((exists ff_h_product_target_successor. ff_h_product_target_successor + S (ff_s_product_target) = S ((S (S ff_i_product_target)) * ff_v_product_target)) /\ exists ff_q_product_target_successor. ff_u_product_target = ff_q_product_target_successor * S ((S (S ff_i_product_target)) * ff_v_product_target) + (ff_s_product_target))) /\ ff_s_product_target = ff_r_product_target * ff_p_product_target)))))) -> T = M * Sprod

Structural proof guide

Generated structural guide

Pointwise products of synchronized beta prefixes multiply their exact finite products.

Use the direct prerequisites beta_product_zero, beta_product_succ_decompose, beta_pointwise_mul_prefix_drop_last, le_refl, one_mul, mul_assoc, mul_comm as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (12), intermediate claims (10), equality transport (8), certified simplification (1).

Referenced ingredients

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA007M beta_pointwise_mul_prefix_drop_last PA001A le_refl PA000M one_mul PA000B mul_assoc PA000H mul_comm

Proof neighborhood

Direct dependencies

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA007M beta_pointwise_mul_prefix_drop_last PA001A le_refl PA000M one_mul PA000B mul_assoc PA000H mul_comm

Direct dependents

PA007O beta_pointwise_mul_product_exists PA0080 gauss_signed_products_balance_mod

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007induction l
  8. 0008intro M
  9. 0009intro Sprod
  10. 0010intro T
  11. 0011intro haligned
  12. 0012intro hM
  13. 0013intro hS
  14. 0014intro hT
  15. 0015have hM1 : M = 1
  16. 0016specialize beta_product_zero mb
  17. 0017specialize beta_product_zero mc
  18. 0018specialize beta_product_zero M
  19. 0019apply beta_product_zero
  20. 0020exact hM
  21. 0021have hS1 : Sprod = 1
  22. 0022specialize beta_product_zero sb
  23. 0023specialize beta_product_zero sc
  24. 0024specialize beta_product_zero Sprod
  25. 0025apply beta_product_zero
  26. 0026exact hS
  27. 0027have hT1 : T = 1
  28. 0028specialize beta_product_zero tb
  29. 0029specialize beta_product_zero tc
  30. 0030specialize beta_product_zero T
  31. 0031apply beta_product_zero
  32. 0032exact hT
  33. 0033rewrite hM1
  34. 0034rewrite hS1
  35. 0035rewrite hT1
  36. 0036specialize one_mul 1
  37. 0037symm
  38. 0038exact one_mul
  39. 0039intro M
  40. 0040intro Sprod
  41. 0041intro T
  42. 0042intro haligned
  43. 0043intro hM
  44. 0044intro hS
  45. 0045intro hT
  46. 0046have hMd : exists fpmp_factor_product_left_decomposition fpmp_prefix_product_left_decomposition. (((exists ff_h_product_left_decomposition_entry. ff_h_product_left_decomposition_entry + S (fpmp_factor_product_left_decomposition) = S ((S (l)) * mc)) /\ exists ff_q_product_left_decomposition_entry. mb = ff_q_product_left_decomposition_entry * S ((S (l)) * mc) + (fpmp_factor_product_left_decomposition))) /\ ((exists ff_u_product_left_decomposition_product ff_v_product_left_decomposition_product. ((((exists ff_h_product_left_decomposition_product_start. ff_h_product_left_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_start. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_start * S ((S (0)) * ff_v_product_left_decomposition_product) + (1))) /\ ((((exists ff_h_product_left_decomposition_product_terminal. ff_h_product_left_decomposition_product_terminal + S (fpmp_prefix_product_left_decomposition) = S ((S (l)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_terminal. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_terminal * S ((S (l)) * ff_v_product_left_decomposition_product) + (fpmp_prefix_product_left_decomposition))) /\ forall ff_i_product_left_decomposition_product. (exists ff_lt_product_left_decomposition_product_bound. ff_lt_product_left_decomposition_product_bound + S ff_i_product_left_decomposition_product = l) -> exists ff_p_product_left_decomposition_product ff_r_product_left_decomposition_product ff_s_product_left_decomposition_product. ((((exists ff_h_product_left_decomposition_product_factor. ff_h_product_left_decomposition_product_factor + S (ff_p_product_left_decomposition_product) = S ((S (ff_i_product_left_decomposition_product)) * mc)) /\ exists ff_q_product_left_decomposition_product_factor. mb = ff_q_product_left_decomposition_product_factor * S ((S (ff_i_product_left_decomposition_product)) * mc) + (ff_p_product_left_decomposition_product))) /\ ((((exists ff_h_product_left_decomposition_product_partial. ff_h_product_left_decomposition_product_partial + S (ff_r_product_left_decomposition_product) = S ((S (ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_partial. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_partial * S ((S (ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product) + (ff_r_product_left_decomposition_product))) /\ ((((exists ff_h_product_left_decomposition_product_successor. ff_h_product_left_decomposition_product_successor + S (ff_s_product_left_decomposition_product) = S ((S (S ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_successor. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_successor * S ((S (S ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product) + (ff_s_product_left_decomposition_product))) /\ ff_s_product_left_decomposition_product = ff_r_product_left_decomposition_product * ff_p_product_left_decomposition_product)))))) /\ M = fpmp_prefix_product_left_decomposition * fpmp_factor_product_left_decomposition)
  47. 0047specialize beta_product_succ_decompose mb
  48. 0048specialize beta_product_succ_decompose mc
  49. 0049specialize beta_product_succ_decompose l
  50. 0050specialize beta_product_succ_decompose M
  51. 0051apply beta_product_succ_decompose
  52. 0052exact hM
  53. 0053cases hMd
  54. 0054cases hMd_witness
  55. 0055cases hMd_witness_witness
  56. 0056cases hMd_witness_witness_right
  57. 0057have hSd : exists fpmp_factor_product_right_decomposition fpmp_prefix_product_right_decomposition. (((exists ff_h_product_right_decomposition_entry. ff_h_product_right_decomposition_entry + S (fpmp_factor_product_right_decomposition) = S ((S (l)) * sc)) /\ exists ff_q_product_right_decomposition_entry. sb = ff_q_product_right_decomposition_entry * S ((S (l)) * sc) + (fpmp_factor_product_right_decomposition))) /\ ((exists ff_u_product_right_decomposition_product ff_v_product_right_decomposition_product. ((((exists ff_h_product_right_decomposition_product_start. ff_h_product_right_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_start. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_start * S ((S (0)) * ff_v_product_right_decomposition_product) + (1))) /\ ((((exists ff_h_product_right_decomposition_product_terminal. ff_h_product_right_decomposition_product_terminal + S (fpmp_prefix_product_right_decomposition) = S ((S (l)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_terminal. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_terminal * S ((S (l)) * ff_v_product_right_decomposition_product) + (fpmp_prefix_product_right_decomposition))) /\ forall ff_i_product_right_decomposition_product. (exists ff_lt_product_right_decomposition_product_bound. ff_lt_product_right_decomposition_product_bound + S ff_i_product_right_decomposition_product = l) -> exists ff_p_product_right_decomposition_product ff_r_product_right_decomposition_product ff_s_product_right_decomposition_product. ((((exists ff_h_product_right_decomposition_product_factor. ff_h_product_right_decomposition_product_factor + S (ff_p_product_right_decomposition_product) = S ((S (ff_i_product_right_decomposition_product)) * sc)) /\ exists ff_q_product_right_decomposition_product_factor. sb = ff_q_product_right_decomposition_product_factor * S ((S (ff_i_product_right_decomposition_product)) * sc) + (ff_p_product_right_decomposition_product))) /\ ((((exists ff_h_product_right_decomposition_product_partial. ff_h_product_right_decomposition_product_partial + S (ff_r_product_right_decomposition_product) = S ((S (ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_partial. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_partial * S ((S (ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product) + (ff_r_product_right_decomposition_product))) /\ ((((exists ff_h_product_right_decomposition_product_successor. ff_h_product_right_decomposition_product_successor + S (ff_s_product_right_decomposition_product) = S ((S (S ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_successor. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_successor * S ((S (S ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product) + (ff_s_product_right_decomposition_product))) /\ ff_s_product_right_decomposition_product = ff_r_product_right_decomposition_product * ff_p_product_right_decomposition_product)))))) /\ Sprod = fpmp_prefix_product_right_decomposition * fpmp_factor_product_right_decomposition)
  58. 0058specialize beta_product_succ_decompose sb
  59. 0059specialize beta_product_succ_decompose sc
  60. 0060specialize beta_product_succ_decompose l
  61. 0061specialize beta_product_succ_decompose Sprod
  62. 0062apply beta_product_succ_decompose
  63. 0063exact hS
  64. 0064cases hSd
  65. 0065cases hSd_witness
  66. 0066cases hSd_witness_witness
  67. 0067cases hSd_witness_witness_right
  68. 0068have hTd : exists fpmp_factor_product_target_decomposition fpmp_prefix_product_target_decomposition. (((exists ff_h_product_target_decomposition_entry. ff_h_product_target_decomposition_entry + S (fpmp_factor_product_target_decomposition) = S ((S (l)) * tc)) /\ exists ff_q_product_target_decomposition_entry. tb = ff_q_product_target_decomposition_entry * S ((S (l)) * tc) + (fpmp_factor_product_target_decomposition))) /\ ((exists ff_u_product_target_decomposition_product ff_v_product_target_decomposition_product. ((((exists ff_h_product_target_decomposition_product_start. ff_h_product_target_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_start. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_start * S ((S (0)) * ff_v_product_target_decomposition_product) + (1))) /\ ((((exists ff_h_product_target_decomposition_product_terminal. ff_h_product_target_decomposition_product_terminal + S (fpmp_prefix_product_target_decomposition) = S ((S (l)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_terminal. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_terminal * S ((S (l)) * ff_v_product_target_decomposition_product) + (fpmp_prefix_product_target_decomposition))) /\ forall ff_i_product_target_decomposition_product. (exists ff_lt_product_target_decomposition_product_bound. ff_lt_product_target_decomposition_product_bound + S ff_i_product_target_decomposition_product = l) -> exists ff_p_product_target_decomposition_product ff_r_product_target_decomposition_product ff_s_product_target_decomposition_product. ((((exists ff_h_product_target_decomposition_product_factor. ff_h_product_target_decomposition_product_factor + S (ff_p_product_target_decomposition_product) = S ((S (ff_i_product_target_decomposition_product)) * tc)) /\ exists ff_q_product_target_decomposition_product_factor. tb = ff_q_product_target_decomposition_product_factor * S ((S (ff_i_product_target_decomposition_product)) * tc) + (ff_p_product_target_decomposition_product))) /\ ((((exists ff_h_product_target_decomposition_product_partial. ff_h_product_target_decomposition_product_partial + S (ff_r_product_target_decomposition_product) = S ((S (ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_partial. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_partial * S ((S (ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product) + (ff_r_product_target_decomposition_product))) /\ ((((exists ff_h_product_target_decomposition_product_successor. ff_h_product_target_decomposition_product_successor + S (ff_s_product_target_decomposition_product) = S ((S (S ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_successor. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_successor * S ((S (S ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product) + (ff_s_product_target_decomposition_product))) /\ ff_s_product_target_decomposition_product = ff_r_product_target_decomposition_product * ff_p_product_target_decomposition_product)))))) /\ T = fpmp_prefix_product_target_decomposition * fpmp_factor_product_target_decomposition)
  69. 0069specialize beta_product_succ_decompose tb
  70. 0070specialize beta_product_succ_decompose tc
  71. 0071specialize beta_product_succ_decompose l
  72. 0072specialize beta_product_succ_decompose T
  73. 0073apply beta_product_succ_decompose
  74. 0074exact hT
  75. 0075cases hTd
  76. 0076cases hTd_witness
  77. 0077cases hTd_witness_witness
  78. 0078cases hTd_witness_witness_right
  79. 0079have hprefix_alignment : forall fpmp_index_product_restricted fpmp_left_product_restricted fpmp_right_product_restricted fpmp_target_product_restricted. (exists fpmp_gap_product_restricted. fpmp_gap_product_restricted + S fpmp_index_product_restricted = l) -> (((exists ff_h_fpmp_product_restricted_left. ff_h_fpmp_product_restricted_left + S (fpmp_left_product_restricted) = S ((S (fpmp_index_product_restricted)) * mc)) /\ exists ff_q_fpmp_product_restricted_left. mb = ff_q_fpmp_product_restricted_left * S ((S (fpmp_index_product_restricted)) * mc) + (fpmp_left_product_restricted))) -> (((exists ff_h_fpmp_product_restricted_right. ff_h_fpmp_product_restricted_right + S (fpmp_right_product_restricted) = S ((S (fpmp_index_product_restricted)) * sc)) /\ exists ff_q_fpmp_product_restricted_right. sb = ff_q_fpmp_product_restricted_right * S ((S (fpmp_index_product_restricted)) * sc) + (fpmp_right_product_restricted))) -> (((exists ff_h_fpmp_product_restricted_target. ff_h_fpmp_product_restricted_target + S (fpmp_target_product_restricted) = S ((S (fpmp_index_product_restricted)) * tc)) /\ exists ff_q_fpmp_product_restricted_target. tb = ff_q_fpmp_product_restricted_target * S ((S (fpmp_index_product_restricted)) * tc) + (fpmp_target_product_restricted))) -> fpmp_target_product_restricted = fpmp_left_product_restricted * fpmp_right_product_restricted
  80. 0080specialize beta_pointwise_mul_prefix_drop_last mb
  81. 0081specialize beta_pointwise_mul_prefix_drop_last mc
  82. 0082specialize beta_pointwise_mul_prefix_drop_last sb
  83. 0083specialize beta_pointwise_mul_prefix_drop_last sc
  84. 0084specialize beta_pointwise_mul_prefix_drop_last tb
  85. 0085specialize beta_pointwise_mul_prefix_drop_last tc
  86. 0086specialize beta_pointwise_mul_prefix_drop_last l
  87. 0087apply beta_pointwise_mul_prefix_drop_last
  88. 0088exact haligned
  89. 0089have hprefix : x5 = x1 * x3
  90. 0090specialize IH x1
  91. 0091specialize IH x3
  92. 0092specialize IH x5
  93. 0093apply IH
  94. 0094exact hprefix_alignment
  95. 0095exact hMd_witness_witness_right_left
  96. 0096exact hSd_witness_witness_right_left
  97. 0097exact hTd_witness_witness_right_left
  98. 0098have hentry : x4 = x * x2
  99. 0099specialize haligned l
  100. 0100specialize haligned x
  101. 0101specialize haligned x2
  102. 0102specialize haligned x4
  103. 0103apply haligned
  104. 0104specialize le_refl (S l)
  105. 0105exact le_refl
  106. 0106exact hMd_witness_witness_left
  107. 0107exact hSd_witness_witness_left
  108. 0108exact hTd_witness_witness_left
  109. 0109have hshuffle : (x1 * x3) * (x * x2) = (x1 * x) * (x3 * x2)
  110. 0110simp [mul_assoc, mul_comm]
  111. 0111rewrite hTd_witness_witness_right_right
  112. 0112rewrite hMd_witness_witness_right_right
  113. 0113rewrite hSd_witness_witness_right_right
  114. 0114rewrite hprefix
  115. 0115rewrite hentry
  116. 0116exact hshuffle