PA007Q

beta_product_pointwise_scale_mod

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

Pointwise multiplication by a constant scales a finite product by its power.

Exact expanded PA statement

forall m a b c z d l P Q A. (forall fsp_index_pointwise fsp_source_pointwise fsp_target_pointwise. (exists fsp_gap_pointwise. fsp_gap_pointwise + S fsp_index_pointwise = l) -> (((exists fsp_source_height_pointwise. fsp_source_height_pointwise + S (fsp_source_pointwise) = S ((S (fsp_index_pointwise)) * c)) /\ exists fsp_source_quotient_pointwise. b = fsp_source_quotient_pointwise * S ((S (fsp_index_pointwise)) * c) + (fsp_source_pointwise))) -> (((exists fsp_target_height_pointwise. fsp_target_height_pointwise + S (fsp_target_pointwise) = S ((S (fsp_index_pointwise)) * d)) /\ exists fsp_target_quotient_pointwise. z = fsp_target_quotient_pointwise * S ((S (fsp_index_pointwise)) * d) + (fsp_target_pointwise))) -> (exists fsp_mod_left_pointwise fsp_mod_right_pointwise. a * fsp_source_pointwise + m * fsp_mod_left_pointwise = fsp_target_pointwise + m * fsp_mod_right_pointwise)) -> (exists ff_u_source ff_v_source. ((((exists ff_h_source_start. ff_h_source_start + S (1) = S ((S (0)) * ff_v_source)) /\ exists ff_q_source_start. ff_u_source = ff_q_source_start * S ((S (0)) * ff_v_source) + (1))) /\ ((((exists ff_h_source_terminal. ff_h_source_terminal + S (P) = S ((S (l)) * ff_v_source)) /\ exists ff_q_source_terminal. ff_u_source = ff_q_source_terminal * S ((S (l)) * ff_v_source) + (P))) /\ forall ff_i_source. (exists ff_lt_source_bound. ff_lt_source_bound + S ff_i_source = l) -> exists ff_p_source ff_r_source ff_s_source. ((((exists ff_h_source_factor. ff_h_source_factor + S (ff_p_source) = S ((S (ff_i_source)) * c)) /\ exists ff_q_source_factor. b = ff_q_source_factor * S ((S (ff_i_source)) * c) + (ff_p_source))) /\ ((((exists ff_h_source_partial. ff_h_source_partial + S (ff_r_source) = S ((S (ff_i_source)) * ff_v_source)) /\ exists ff_q_source_partial. ff_u_source = ff_q_source_partial * S ((S (ff_i_source)) * ff_v_source) + (ff_r_source))) /\ ((((exists ff_h_source_successor. ff_h_source_successor + S (ff_s_source) = S ((S (S ff_i_source)) * ff_v_source)) /\ exists ff_q_source_successor. ff_u_source = ff_q_source_successor * S ((S (S ff_i_source)) * ff_v_source) + (ff_s_source))) /\ ff_s_source = ff_r_source * ff_p_source)))))) -> (exists ff_u_target ff_v_target. ((((exists ff_h_target_start. ff_h_target_start + S (1) = S ((S (0)) * ff_v_target)) /\ exists ff_q_target_start. ff_u_target = ff_q_target_start * S ((S (0)) * ff_v_target) + (1))) /\ ((((exists ff_h_target_terminal. ff_h_target_terminal + S (Q) = S ((S (l)) * ff_v_target)) /\ exists ff_q_target_terminal. ff_u_target = ff_q_target_terminal * S ((S (l)) * ff_v_target) + (Q))) /\ forall ff_i_target. (exists ff_lt_target_bound. ff_lt_target_bound + S ff_i_target = l) -> exists ff_p_target ff_r_target ff_s_target. ((((exists ff_h_target_factor. ff_h_target_factor + S (ff_p_target) = S ((S (ff_i_target)) * d)) /\ exists ff_q_target_factor. z = ff_q_target_factor * S ((S (ff_i_target)) * d) + (ff_p_target))) /\ ((((exists ff_h_target_partial. ff_h_target_partial + S (ff_r_target) = S ((S (ff_i_target)) * ff_v_target)) /\ exists ff_q_target_partial. ff_u_target = ff_q_target_partial * S ((S (ff_i_target)) * ff_v_target) + (ff_r_target))) /\ ((((exists ff_h_target_successor. ff_h_target_successor + S (ff_s_target) = S ((S (S ff_i_target)) * ff_v_target)) /\ exists ff_q_target_successor. ff_u_target = ff_q_target_successor * S ((S (S ff_i_target)) * ff_v_target) + (ff_s_target))) /\ ff_s_target = ff_r_target * ff_p_target)))))) -> (exists ff_b_scale_power ff_c_scale_power. ((forall ff_i_scale_power_repeat. (exists ff_lt_scale_power_repeat_bound. ff_lt_scale_power_repeat_bound + S ff_i_scale_power_repeat = l) -> (((exists ff_h_scale_power_repeat_decoded. ff_h_scale_power_repeat_decoded + S (a) = S ((S (ff_i_scale_power_repeat)) * ff_c_scale_power)) /\ exists ff_q_scale_power_repeat_decoded. ff_b_scale_power = ff_q_scale_power_repeat_decoded * S ((S (ff_i_scale_power_repeat)) * ff_c_scale_power) + (a)))) /\ (exists ff_u_scale_power_product ff_v_scale_power_product. ((((exists ff_h_scale_power_product_start. ff_h_scale_power_product_start + S (1) = S ((S (0)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_start. ff_u_scale_power_product = ff_q_scale_power_product_start * S ((S (0)) * ff_v_scale_power_product) + (1))) /\ ((((exists ff_h_scale_power_product_terminal. ff_h_scale_power_product_terminal + S (A) = S ((S (l)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_terminal. ff_u_scale_power_product = ff_q_scale_power_product_terminal * S ((S (l)) * ff_v_scale_power_product) + (A))) /\ forall ff_i_scale_power_product. (exists ff_lt_scale_power_product_bound. ff_lt_scale_power_product_bound + S ff_i_scale_power_product = l) -> exists ff_p_scale_power_product ff_r_scale_power_product ff_s_scale_power_product. ((((exists ff_h_scale_power_product_factor. ff_h_scale_power_product_factor + S (ff_p_scale_power_product) = S ((S (ff_i_scale_power_product)) * ff_c_scale_power)) /\ exists ff_q_scale_power_product_factor. ff_b_scale_power = ff_q_scale_power_product_factor * S ((S (ff_i_scale_power_product)) * ff_c_scale_power) + (ff_p_scale_power_product))) /\ ((((exists ff_h_scale_power_product_partial. ff_h_scale_power_product_partial + S (ff_r_scale_power_product) = S ((S (ff_i_scale_power_product)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_partial. ff_u_scale_power_product = ff_q_scale_power_product_partial * S ((S (ff_i_scale_power_product)) * ff_v_scale_power_product) + (ff_r_scale_power_product))) /\ ((((exists ff_h_scale_power_product_successor. ff_h_scale_power_product_successor + S (ff_s_scale_power_product) = S ((S (S ff_i_scale_power_product)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_successor. ff_u_scale_power_product = ff_q_scale_power_product_successor * S ((S (S ff_i_scale_power_product)) * ff_v_scale_power_product) + (ff_s_scale_power_product))) /\ ff_s_scale_power_product = ff_r_scale_power_product * ff_p_scale_power_product)))))))) -> (exists fsp_product_mod_left_result fsp_product_mod_right_result. (A * P) + m * fsp_product_mod_left_result = Q + m * fsp_product_mod_right_result)

Structural proof guide

Generated structural guide

Pointwise multiplication by a constant scales a finite product by its power.

Use the direct prerequisites beta_product_zero, beta_product_succ_decompose, pow_zero, pow_successor_decompose, le_succ, le_refl, mod_eq_refl, mod_eq_mul, mul_assoc, mul_comm, one_mul as previously established PA formulas.

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

Referenced ingredients

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004B pow_zero PA004D pow_successor_decompose PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000B mul_assoc PA000H mul_comm PA000M one_mul

Proof neighborhood

Direct dependencies

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004B pow_zero PA004D pow_successor_decompose PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000B mul_assoc PA000H mul_comm PA000M one_mul

Direct dependents

PA007R gauss_signed_pointwise_mul_product_mod PA008J prime_mul_residue_product_balance

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 m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007induction l
  8. 0008intro P
  9. 0009intro Q
  10. 0010intro A
  11. 0011intro hpw
  12. 0012intro hP
  13. 0013intro hQ
  14. 0014intro hA
  15. 0015have hP1 : P = 1
  16. 0016specialize beta_product_zero b
  17. 0017specialize beta_product_zero c
  18. 0018specialize beta_product_zero P
  19. 0019apply beta_product_zero
  20. 0020exact hP
  21. 0021have hQ1 : Q = 1
  22. 0022specialize beta_product_zero z
  23. 0023specialize beta_product_zero d
  24. 0024specialize beta_product_zero Q
  25. 0025apply beta_product_zero
  26. 0026exact hQ
  27. 0027have hA1 : A = 1
  28. 0028specialize pow_zero a
  29. 0029specialize pow_zero 0
  30. 0030specialize pow_zero A
  31. 0031apply pow_zero
  32. 0032refl
  33. 0033exact hA
  34. 0034rewrite hA1
  35. 0035rewrite hP1
  36. 0036rewrite hQ1
  37. 0037have hone : 1 * 1 = 1
  38. 0038specialize one_mul 1
  39. 0039exact one_mul
  40. 0040rewrite hone
  41. 0041specialize mod_eq_refl m
  42. 0042specialize mod_eq_refl 1
  43. 0043exact mod_eq_refl
  44. 0044intro P
  45. 0045intro Q
  46. 0046intro A
  47. 0047intro hpw
  48. 0048intro hP
  49. 0049intro hQ
  50. 0050intro hA
  51. 0051have hPd : exists fsp_decomposition_factor_source_decomposition fsp_decomposition_prefix_source_decomposition. (((exists ff_h_source_decomposition_factor. ff_h_source_decomposition_factor + S (fsp_decomposition_factor_source_decomposition) = S ((S (l)) * c)) /\ exists ff_q_source_decomposition_factor. b = ff_q_source_decomposition_factor * S ((S (l)) * c) + (fsp_decomposition_factor_source_decomposition))) /\ ((exists ff_u_source_decomposition_prefix ff_v_source_decomposition_prefix. ((((exists ff_h_source_decomposition_prefix_start. ff_h_source_decomposition_prefix_start + S (1) = S ((S (0)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_start. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_start * S ((S (0)) * ff_v_source_decomposition_prefix) + (1))) /\ ((((exists ff_h_source_decomposition_prefix_terminal. ff_h_source_decomposition_prefix_terminal + S (fsp_decomposition_prefix_source_decomposition) = S ((S (l)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_terminal. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_terminal * S ((S (l)) * ff_v_source_decomposition_prefix) + (fsp_decomposition_prefix_source_decomposition))) /\ forall ff_i_source_decomposition_prefix. (exists ff_lt_source_decomposition_prefix_bound. ff_lt_source_decomposition_prefix_bound + S ff_i_source_decomposition_prefix = l) -> exists ff_p_source_decomposition_prefix ff_r_source_decomposition_prefix ff_s_source_decomposition_prefix. ((((exists ff_h_source_decomposition_prefix_factor. ff_h_source_decomposition_prefix_factor + S (ff_p_source_decomposition_prefix) = S ((S (ff_i_source_decomposition_prefix)) * c)) /\ exists ff_q_source_decomposition_prefix_factor. b = ff_q_source_decomposition_prefix_factor * S ((S (ff_i_source_decomposition_prefix)) * c) + (ff_p_source_decomposition_prefix))) /\ ((((exists ff_h_source_decomposition_prefix_partial. ff_h_source_decomposition_prefix_partial + S (ff_r_source_decomposition_prefix) = S ((S (ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_partial. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_partial * S ((S (ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix) + (ff_r_source_decomposition_prefix))) /\ ((((exists ff_h_source_decomposition_prefix_successor. ff_h_source_decomposition_prefix_successor + S (ff_s_source_decomposition_prefix) = S ((S (S ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_successor. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_successor * S ((S (S ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix) + (ff_s_source_decomposition_prefix))) /\ ff_s_source_decomposition_prefix = ff_r_source_decomposition_prefix * ff_p_source_decomposition_prefix)))))) /\ P = fsp_decomposition_prefix_source_decomposition * fsp_decomposition_factor_source_decomposition)
  52. 0052specialize beta_product_succ_decompose b
  53. 0053specialize beta_product_succ_decompose c
  54. 0054specialize beta_product_succ_decompose l
  55. 0055specialize beta_product_succ_decompose P
  56. 0056apply beta_product_succ_decompose
  57. 0057exact hP
  58. 0058cases hPd
  59. 0059cases hPd_witness
  60. 0060cases hPd_witness_witness
  61. 0061cases hPd_witness_witness_right
  62. 0062have hQd : exists fsp_decomposition_factor_target_decomposition fsp_decomposition_prefix_target_decomposition. (((exists ff_h_target_decomposition_factor. ff_h_target_decomposition_factor + S (fsp_decomposition_factor_target_decomposition) = S ((S (l)) * d)) /\ exists ff_q_target_decomposition_factor. z = ff_q_target_decomposition_factor * S ((S (l)) * d) + (fsp_decomposition_factor_target_decomposition))) /\ ((exists ff_u_target_decomposition_prefix ff_v_target_decomposition_prefix. ((((exists ff_h_target_decomposition_prefix_start. ff_h_target_decomposition_prefix_start + S (1) = S ((S (0)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_start. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_start * S ((S (0)) * ff_v_target_decomposition_prefix) + (1))) /\ ((((exists ff_h_target_decomposition_prefix_terminal. ff_h_target_decomposition_prefix_terminal + S (fsp_decomposition_prefix_target_decomposition) = S ((S (l)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_terminal. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_terminal * S ((S (l)) * ff_v_target_decomposition_prefix) + (fsp_decomposition_prefix_target_decomposition))) /\ forall ff_i_target_decomposition_prefix. (exists ff_lt_target_decomposition_prefix_bound. ff_lt_target_decomposition_prefix_bound + S ff_i_target_decomposition_prefix = l) -> exists ff_p_target_decomposition_prefix ff_r_target_decomposition_prefix ff_s_target_decomposition_prefix. ((((exists ff_h_target_decomposition_prefix_factor. ff_h_target_decomposition_prefix_factor + S (ff_p_target_decomposition_prefix) = S ((S (ff_i_target_decomposition_prefix)) * d)) /\ exists ff_q_target_decomposition_prefix_factor. z = ff_q_target_decomposition_prefix_factor * S ((S (ff_i_target_decomposition_prefix)) * d) + (ff_p_target_decomposition_prefix))) /\ ((((exists ff_h_target_decomposition_prefix_partial. ff_h_target_decomposition_prefix_partial + S (ff_r_target_decomposition_prefix) = S ((S (ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_partial. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_partial * S ((S (ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix) + (ff_r_target_decomposition_prefix))) /\ ((((exists ff_h_target_decomposition_prefix_successor. ff_h_target_decomposition_prefix_successor + S (ff_s_target_decomposition_prefix) = S ((S (S ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_successor. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_successor * S ((S (S ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix) + (ff_s_target_decomposition_prefix))) /\ ff_s_target_decomposition_prefix = ff_r_target_decomposition_prefix * ff_p_target_decomposition_prefix)))))) /\ Q = fsp_decomposition_prefix_target_decomposition * fsp_decomposition_factor_target_decomposition)
  63. 0063specialize beta_product_succ_decompose z
  64. 0064specialize beta_product_succ_decompose d
  65. 0065specialize beta_product_succ_decompose l
  66. 0066specialize beta_product_succ_decompose Q
  67. 0067apply beta_product_succ_decompose
  68. 0068exact hQ
  69. 0069cases hQd
  70. 0070cases hQd_witness
  71. 0071cases hQd_witness_witness
  72. 0072cases hQd_witness_witness_right
  73. 0073have hAd : exists fsp_power_prefix_power_decomposition. (exists ff_b_power_decomposition_relation ff_c_power_decomposition_relation. ((forall ff_i_power_decomposition_relation_repeat. (exists ff_lt_power_decomposition_relation_repeat_bound. ff_lt_power_decomposition_relation_repeat_bound + S ff_i_power_decomposition_relation_repeat = l) -> (((exists ff_h_power_decomposition_relation_repeat_decoded. ff_h_power_decomposition_relation_repeat_decoded + S (a) = S ((S (ff_i_power_decomposition_relation_repeat)) * ff_c_power_decomposition_relation)) /\ exists ff_q_power_decomposition_relation_repeat_decoded. ff_b_power_decomposition_relation = ff_q_power_decomposition_relation_repeat_decoded * S ((S (ff_i_power_decomposition_relation_repeat)) * ff_c_power_decomposition_relation) + (a)))) /\ (exists ff_u_power_decomposition_relation_product ff_v_power_decomposition_relation_product. ((((exists ff_h_power_decomposition_relation_product_start. ff_h_power_decomposition_relation_product_start + S (1) = S ((S (0)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_start. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_start * S ((S (0)) * ff_v_power_decomposition_relation_product) + (1))) /\ ((((exists ff_h_power_decomposition_relation_product_terminal. ff_h_power_decomposition_relation_product_terminal + S (fsp_power_prefix_power_decomposition) = S ((S (l)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_terminal. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_terminal * S ((S (l)) * ff_v_power_decomposition_relation_product) + (fsp_power_prefix_power_decomposition))) /\ forall ff_i_power_decomposition_relation_product. (exists ff_lt_power_decomposition_relation_product_bound. ff_lt_power_decomposition_relation_product_bound + S ff_i_power_decomposition_relation_product = l) -> exists ff_p_power_decomposition_relation_product ff_r_power_decomposition_relation_product ff_s_power_decomposition_relation_product. ((((exists ff_h_power_decomposition_relation_product_factor. ff_h_power_decomposition_relation_product_factor + S (ff_p_power_decomposition_relation_product) = S ((S (ff_i_power_decomposition_relation_product)) * ff_c_power_decomposition_relation)) /\ exists ff_q_power_decomposition_relation_product_factor. ff_b_power_decomposition_relation = ff_q_power_decomposition_relation_product_factor * S ((S (ff_i_power_decomposition_relation_product)) * ff_c_power_decomposition_relation) + (ff_p_power_decomposition_relation_product))) /\ ((((exists ff_h_power_decomposition_relation_product_partial. ff_h_power_decomposition_relation_product_partial + S (ff_r_power_decomposition_relation_product) = S ((S (ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_partial. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_partial * S ((S (ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product) + (ff_r_power_decomposition_relation_product))) /\ ((((exists ff_h_power_decomposition_relation_product_successor. ff_h_power_decomposition_relation_product_successor + S (ff_s_power_decomposition_relation_product) = S ((S (S ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_successor. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_successor * S ((S (S ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product) + (ff_s_power_decomposition_relation_product))) /\ ff_s_power_decomposition_relation_product = ff_r_power_decomposition_relation_product * ff_p_power_decomposition_relation_product)))))))) /\ A = fsp_power_prefix_power_decomposition * a
  74. 0074specialize pow_successor_decompose a
  75. 0075specialize pow_successor_decompose l
  76. 0076specialize pow_successor_decompose (S l)
  77. 0077specialize pow_successor_decompose A
  78. 0078apply pow_successor_decompose
  79. 0079refl
  80. 0080exact hA
  81. 0081cases hAd
  82. 0082cases hAd_witness
  83. 0083have hpw_prefix : forall fsp_index_pointwise_prefix fsp_source_pointwise_prefix fsp_target_pointwise_prefix. (exists fsp_gap_pointwise_prefix. fsp_gap_pointwise_prefix + S fsp_index_pointwise_prefix = l) -> (((exists fsp_source_height_pointwise_prefix. fsp_source_height_pointwise_prefix + S (fsp_source_pointwise_prefix) = S ((S (fsp_index_pointwise_prefix)) * c)) /\ exists fsp_source_quotient_pointwise_prefix. b = fsp_source_quotient_pointwise_prefix * S ((S (fsp_index_pointwise_prefix)) * c) + (fsp_source_pointwise_prefix))) -> (((exists fsp_target_height_pointwise_prefix. fsp_target_height_pointwise_prefix + S (fsp_target_pointwise_prefix) = S ((S (fsp_index_pointwise_prefix)) * d)) /\ exists fsp_target_quotient_pointwise_prefix. z = fsp_target_quotient_pointwise_prefix * S ((S (fsp_index_pointwise_prefix)) * d) + (fsp_target_pointwise_prefix))) -> (exists fsp_mod_left_pointwise_prefix fsp_mod_right_pointwise_prefix. a * fsp_source_pointwise_prefix + m * fsp_mod_left_pointwise_prefix = fsp_target_pointwise_prefix + m * fsp_mod_right_pointwise_prefix)
  84. 0084intro i
  85. 0085intro v
  86. 0086intro w
  87. 0087intro hi
  88. 0088intro hv
  89. 0089intro hw
  90. 0090specialize hpw i
  91. 0091specialize hpw v
  92. 0092specialize hpw w
  93. 0093apply hpw
  94. 0094specialize le_succ (S i)
  95. 0095specialize le_succ l
  96. 0096apply le_succ
  97. 0097exact hi
  98. 0098exact hv
  99. 0099exact hw
  100. 0100have hprefix : exists u v. (x4 * x1) + m * u = x3 + m * v
  101. 0101specialize IH x1
  102. 0102specialize IH x3
  103. 0103specialize IH x4
  104. 0104apply IH
  105. 0105exact hpw_prefix
  106. 0106exact hPd_witness_witness_right_left
  107. 0107exact hQd_witness_witness_right_left
  108. 0108exact hAd_witness_left
  109. 0109have hentry : exists u v. (a * x) + m * u = x2 + m * v
  110. 0110specialize hpw l
  111. 0111specialize hpw x
  112. 0112specialize hpw x2
  113. 0113apply hpw
  114. 0114specialize le_refl (S l)
  115. 0115exact le_refl
  116. 0116exact hPd_witness_witness_left
  117. 0117exact hQd_witness_witness_left
  118. 0118have hfold : exists u v. ((x4 * x1) * (a * x)) + m * u = (x3 * x2) + m * v
  119. 0119specialize mod_eq_mul m
  120. 0120specialize mod_eq_mul (x4 * x1)
  121. 0121specialize mod_eq_mul x3
  122. 0122specialize mod_eq_mul (a * x)
  123. 0123specialize mod_eq_mul x2
  124. 0124apply mod_eq_mul
  125. 0125exact hprefix
  126. 0126exact hentry
  127. 0127have hshuffle : (x4 * a) * (x1 * x) = (x4 * x1) * (a * x)
  128. 0128simp [mul_assoc, mul_comm]
  129. 0129rewrite hAd_witness_right
  130. 0130rewrite hPd_witness_witness_right_right
  131. 0131rewrite hQd_witness_witness_right_right
  132. 0132rewrite hshuffle
  133. 0133exact hfold