BT00K5

beta_sum_pointwise_add

Alpha body-checked · checked-use disabled

Pointwise sums of decoded entries induce exact addition of finite sums.

Exact expanded PA statement

forall b c d e f g l n m q. (exists ff_u_pointadd_left ff_v_pointadd_left. ((((exists ff_h_pointadd_left_start. ff_h_pointadd_left_start + S (0) = S ((S (0)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_start. ff_u_pointadd_left = ff_q_pointadd_left_start * S ((S (0)) * ff_v_pointadd_left) + (0))) /\ ((((exists ff_h_pointadd_left_terminal. ff_h_pointadd_left_terminal + S (n) = S ((S (l)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_terminal. ff_u_pointadd_left = ff_q_pointadd_left_terminal * S ((S (l)) * ff_v_pointadd_left) + (n))) /\ forall ff_i_pointadd_left. (exists ff_lt_pointadd_left_bound. ff_lt_pointadd_left_bound + S ff_i_pointadd_left = l) -> exists ff_a_pointadd_left ff_r_pointadd_left ff_s_pointadd_left. ((((exists ff_h_pointadd_left_summand. ff_h_pointadd_left_summand + S (ff_a_pointadd_left) = S ((S (ff_i_pointadd_left)) * c)) /\ exists ff_q_pointadd_left_summand. b = ff_q_pointadd_left_summand * S ((S (ff_i_pointadd_left)) * c) + (ff_a_pointadd_left))) /\ ((((exists ff_h_pointadd_left_partial. ff_h_pointadd_left_partial + S (ff_r_pointadd_left) = S ((S (ff_i_pointadd_left)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_partial. ff_u_pointadd_left = ff_q_pointadd_left_partial * S ((S (ff_i_pointadd_left)) * ff_v_pointadd_left) + (ff_r_pointadd_left))) /\ ((((exists ff_h_pointadd_left_successor. ff_h_pointadd_left_successor + S (ff_s_pointadd_left) = S ((S (S ff_i_pointadd_left)) * ff_v_pointadd_left)) /\ exists ff_q_pointadd_left_successor. ff_u_pointadd_left = ff_q_pointadd_left_successor * S ((S (S ff_i_pointadd_left)) * ff_v_pointadd_left) + (ff_s_pointadd_left))) /\ ff_s_pointadd_left = ff_r_pointadd_left + ff_a_pointadd_left)))))) -> (exists ff_u_pointadd_right ff_v_pointadd_right. ((((exists ff_h_pointadd_right_start. ff_h_pointadd_right_start + S (0) = S ((S (0)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_start. ff_u_pointadd_right = ff_q_pointadd_right_start * S ((S (0)) * ff_v_pointadd_right) + (0))) /\ ((((exists ff_h_pointadd_right_terminal. ff_h_pointadd_right_terminal + S (m) = S ((S (l)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_terminal. ff_u_pointadd_right = ff_q_pointadd_right_terminal * S ((S (l)) * ff_v_pointadd_right) + (m))) /\ forall ff_i_pointadd_right. (exists ff_lt_pointadd_right_bound. ff_lt_pointadd_right_bound + S ff_i_pointadd_right = l) -> exists ff_a_pointadd_right ff_r_pointadd_right ff_s_pointadd_right. ((((exists ff_h_pointadd_right_summand. ff_h_pointadd_right_summand + S (ff_a_pointadd_right) = S ((S (ff_i_pointadd_right)) * e)) /\ exists ff_q_pointadd_right_summand. d = ff_q_pointadd_right_summand * S ((S (ff_i_pointadd_right)) * e) + (ff_a_pointadd_right))) /\ ((((exists ff_h_pointadd_right_partial. ff_h_pointadd_right_partial + S (ff_r_pointadd_right) = S ((S (ff_i_pointadd_right)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_partial. ff_u_pointadd_right = ff_q_pointadd_right_partial * S ((S (ff_i_pointadd_right)) * ff_v_pointadd_right) + (ff_r_pointadd_right))) /\ ((((exists ff_h_pointadd_right_successor. ff_h_pointadd_right_successor + S (ff_s_pointadd_right) = S ((S (S ff_i_pointadd_right)) * ff_v_pointadd_right)) /\ exists ff_q_pointadd_right_successor. ff_u_pointadd_right = ff_q_pointadd_right_successor * S ((S (S ff_i_pointadd_right)) * ff_v_pointadd_right) + (ff_s_pointadd_right))) /\ ff_s_pointadd_right = ff_r_pointadd_right + ff_a_pointadd_right)))))) -> (exists ff_u_pointadd_total ff_v_pointadd_total. ((((exists ff_h_pointadd_total_start. ff_h_pointadd_total_start + S (0) = S ((S (0)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_start. ff_u_pointadd_total = ff_q_pointadd_total_start * S ((S (0)) * ff_v_pointadd_total) + (0))) /\ ((((exists ff_h_pointadd_total_terminal. ff_h_pointadd_total_terminal + S (q) = S ((S (l)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_terminal. ff_u_pointadd_total = ff_q_pointadd_total_terminal * S ((S (l)) * ff_v_pointadd_total) + (q))) /\ forall ff_i_pointadd_total. (exists ff_lt_pointadd_total_bound. ff_lt_pointadd_total_bound + S ff_i_pointadd_total = l) -> exists ff_a_pointadd_total ff_r_pointadd_total ff_s_pointadd_total. ((((exists ff_h_pointadd_total_summand. ff_h_pointadd_total_summand + S (ff_a_pointadd_total) = S ((S (ff_i_pointadd_total)) * g)) /\ exists ff_q_pointadd_total_summand. f = ff_q_pointadd_total_summand * S ((S (ff_i_pointadd_total)) * g) + (ff_a_pointadd_total))) /\ ((((exists ff_h_pointadd_total_partial. ff_h_pointadd_total_partial + S (ff_r_pointadd_total) = S ((S (ff_i_pointadd_total)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_partial. ff_u_pointadd_total = ff_q_pointadd_total_partial * S ((S (ff_i_pointadd_total)) * ff_v_pointadd_total) + (ff_r_pointadd_total))) /\ ((((exists ff_h_pointadd_total_successor. ff_h_pointadd_total_successor + S (ff_s_pointadd_total) = S ((S (S ff_i_pointadd_total)) * ff_v_pointadd_total)) /\ exists ff_q_pointadd_total_successor. ff_u_pointadd_total = ff_q_pointadd_total_successor * S ((S (S ff_i_pointadd_total)) * ff_v_pointadd_total) + (ff_s_pointadd_total))) /\ ff_s_pointadd_total = ff_r_pointadd_total + ff_a_pointadd_total)))))) -> (forall i a z s. (exists h. h + S i = l) -> (((exists ff_h_pointadd_left_entry. ff_h_pointadd_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pointadd_left_entry. b = ff_q_pointadd_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_pointadd_right_entry. ff_h_pointadd_right_entry + S (z) = S ((S (i)) * e)) /\ exists ff_q_pointadd_right_entry. d = ff_q_pointadd_right_entry * S ((S (i)) * e) + (z))) -> (((exists ff_h_pointadd_total_entry. ff_h_pointadd_total_entry + S (s) = S ((S (i)) * g)) /\ exists ff_q_pointadd_total_entry. f = ff_q_pointadd_total_entry * S ((S (i)) * g) + (s))) -> s = a + z) -> n + m = q

Structural proof guide

Pointwise sums of decoded entries induce exact addition of finite sums.

Direct prerequisites: beta_sum_zero, beta_sum_succ_decompose, le_succ, le_refl, add_assoc, add_comm. The authored body proceeds by structural induction (1), case analysis (12), intermediate claims (9), equality transport (8).

Proof neighborhood

Direct dependencies

BT008E beta_sum_zero BT008F beta_sum_succ_decompose BT0018 le_succ BT000E le_refl BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00SV prime_legendre_sum_succ

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007induction l
  8. 0008intro n
  9. 0009intro m
  10. 0010intro q
  11. 0011intro hleft
  12. 0012intro hright
  13. 0013intro htotal
  14. 0014intro hpointwise
  15. 0015have hn : n = 0
  16. 0016specialize beta_sum_zero b
  17. 0017specialize beta_sum_zero c
  18. 0018specialize beta_sum_zero n
  19. 0019apply beta_sum_zero
  20. 0020exact hleft
  21. 0021have hm : m = 0
  22. 0022specialize beta_sum_zero d
  23. 0023specialize beta_sum_zero e
  24. 0024specialize beta_sum_zero m
  25. 0025apply beta_sum_zero
  26. 0026exact hright
  27. 0027have hq : q = 0
  28. 0028specialize beta_sum_zero f
  29. 0029specialize beta_sum_zero g
  30. 0030specialize beta_sum_zero q
  31. 0031apply beta_sum_zero
  32. 0032exact htotal
  33. 0033rewrite hn
  34. 0034rewrite hm
  35. 0035rewrite hq
  36. 0036simp
  37. 0037intro n
  38. 0038intro m
  39. 0039intro q
  40. 0040intro hleft
  41. 0041intro hright
  42. 0042intro htotal
  43. 0043intro hpointwise
  44. 0044have hleft_decomp : exists a r. (((exists ff_h_pointadd_left_decomp_entry. ff_h_pointadd_left_decomp_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_pointadd_left_decomp_entry. b = ff_q_pointadd_left_decomp_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_pointadd_left_decomp_prefix ff_v_pointadd_left_decomp_prefix. ((((exists ff_h_pointadd_left_decomp_prefix_start. ff_h_pointadd_left_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_start. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_left_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_terminal. ff_h_pointadd_left_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_terminal. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_left_decomp_prefix) + (r))) /\ forall ff_i_pointadd_left_decomp_prefix. (exists ff_lt_pointadd_left_decomp_prefix_bound. ff_lt_pointadd_left_decomp_prefix_bound + S ff_i_pointadd_left_decomp_prefix = l) -> exists ff_a_pointadd_left_decomp_prefix ff_r_pointadd_left_decomp_prefix ff_s_pointadd_left_decomp_prefix. ((((exists ff_h_pointadd_left_decomp_prefix_summand. ff_h_pointadd_left_decomp_prefix_summand + S (ff_a_pointadd_left_decomp_prefix) = S ((S (ff_i_pointadd_left_decomp_prefix)) * c)) /\ exists ff_q_pointadd_left_decomp_prefix_summand. b = ff_q_pointadd_left_decomp_prefix_summand * S ((S (ff_i_pointadd_left_decomp_prefix)) * c) + (ff_a_pointadd_left_decomp_prefix))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_partial. ff_h_pointadd_left_decomp_prefix_partial + S (ff_r_pointadd_left_decomp_prefix) = S ((S (ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_partial. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_partial * S ((S (ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix) + (ff_r_pointadd_left_decomp_prefix))) /\ ((((exists ff_h_pointadd_left_decomp_prefix_successor. ff_h_pointadd_left_decomp_prefix_successor + S (ff_s_pointadd_left_decomp_prefix) = S ((S (S ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix)) /\ exists ff_q_pointadd_left_decomp_prefix_successor. ff_u_pointadd_left_decomp_prefix = ff_q_pointadd_left_decomp_prefix_successor * S ((S (S ff_i_pointadd_left_decomp_prefix)) * ff_v_pointadd_left_decomp_prefix) + (ff_s_pointadd_left_decomp_prefix))) /\ ff_s_pointadd_left_decomp_prefix = ff_r_pointadd_left_decomp_prefix + ff_a_pointadd_left_decomp_prefix)))))) /\ n = r + a)
  45. 0045specialize beta_sum_succ_decompose b
  46. 0046specialize beta_sum_succ_decompose c
  47. 0047specialize beta_sum_succ_decompose l
  48. 0048specialize beta_sum_succ_decompose n
  49. 0049apply beta_sum_succ_decompose
  50. 0050exact hleft
  51. 0051cases hleft_decomp
  52. 0052cases hleft_decomp_witness
  53. 0053cases hleft_decomp_witness_witness
  54. 0054cases hleft_decomp_witness_witness_right
  55. 0055have hright_decomp : exists a r. (((exists ff_h_pointadd_right_decomp_entry. ff_h_pointadd_right_decomp_entry + S (a) = S ((S (l)) * e)) /\ exists ff_q_pointadd_right_decomp_entry. d = ff_q_pointadd_right_decomp_entry * S ((S (l)) * e) + (a))) /\ ((exists ff_u_pointadd_right_decomp_prefix ff_v_pointadd_right_decomp_prefix. ((((exists ff_h_pointadd_right_decomp_prefix_start. ff_h_pointadd_right_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_start. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_right_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_terminal. ff_h_pointadd_right_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_terminal. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_right_decomp_prefix) + (r))) /\ forall ff_i_pointadd_right_decomp_prefix. (exists ff_lt_pointadd_right_decomp_prefix_bound. ff_lt_pointadd_right_decomp_prefix_bound + S ff_i_pointadd_right_decomp_prefix = l) -> exists ff_a_pointadd_right_decomp_prefix ff_r_pointadd_right_decomp_prefix ff_s_pointadd_right_decomp_prefix. ((((exists ff_h_pointadd_right_decomp_prefix_summand. ff_h_pointadd_right_decomp_prefix_summand + S (ff_a_pointadd_right_decomp_prefix) = S ((S (ff_i_pointadd_right_decomp_prefix)) * e)) /\ exists ff_q_pointadd_right_decomp_prefix_summand. d = ff_q_pointadd_right_decomp_prefix_summand * S ((S (ff_i_pointadd_right_decomp_prefix)) * e) + (ff_a_pointadd_right_decomp_prefix))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_partial. ff_h_pointadd_right_decomp_prefix_partial + S (ff_r_pointadd_right_decomp_prefix) = S ((S (ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_partial. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_partial * S ((S (ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix) + (ff_r_pointadd_right_decomp_prefix))) /\ ((((exists ff_h_pointadd_right_decomp_prefix_successor. ff_h_pointadd_right_decomp_prefix_successor + S (ff_s_pointadd_right_decomp_prefix) = S ((S (S ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix)) /\ exists ff_q_pointadd_right_decomp_prefix_successor. ff_u_pointadd_right_decomp_prefix = ff_q_pointadd_right_decomp_prefix_successor * S ((S (S ff_i_pointadd_right_decomp_prefix)) * ff_v_pointadd_right_decomp_prefix) + (ff_s_pointadd_right_decomp_prefix))) /\ ff_s_pointadd_right_decomp_prefix = ff_r_pointadd_right_decomp_prefix + ff_a_pointadd_right_decomp_prefix)))))) /\ m = r + a)
  56. 0056specialize beta_sum_succ_decompose d
  57. 0057specialize beta_sum_succ_decompose e
  58. 0058specialize beta_sum_succ_decompose l
  59. 0059specialize beta_sum_succ_decompose m
  60. 0060apply beta_sum_succ_decompose
  61. 0061exact hright
  62. 0062cases hright_decomp
  63. 0063cases hright_decomp_witness
  64. 0064cases hright_decomp_witness_witness
  65. 0065cases hright_decomp_witness_witness_right
  66. 0066have htotal_decomp : exists a r. (((exists ff_h_pointadd_total_decomp_entry. ff_h_pointadd_total_decomp_entry + S (a) = S ((S (l)) * g)) /\ exists ff_q_pointadd_total_decomp_entry. f = ff_q_pointadd_total_decomp_entry * S ((S (l)) * g) + (a))) /\ ((exists ff_u_pointadd_total_decomp_prefix ff_v_pointadd_total_decomp_prefix. ((((exists ff_h_pointadd_total_decomp_prefix_start. ff_h_pointadd_total_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_start. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_start * S ((S (0)) * ff_v_pointadd_total_decomp_prefix) + (0))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_terminal. ff_h_pointadd_total_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_terminal. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_terminal * S ((S (l)) * ff_v_pointadd_total_decomp_prefix) + (r))) /\ forall ff_i_pointadd_total_decomp_prefix. (exists ff_lt_pointadd_total_decomp_prefix_bound. ff_lt_pointadd_total_decomp_prefix_bound + S ff_i_pointadd_total_decomp_prefix = l) -> exists ff_a_pointadd_total_decomp_prefix ff_r_pointadd_total_decomp_prefix ff_s_pointadd_total_decomp_prefix. ((((exists ff_h_pointadd_total_decomp_prefix_summand. ff_h_pointadd_total_decomp_prefix_summand + S (ff_a_pointadd_total_decomp_prefix) = S ((S (ff_i_pointadd_total_decomp_prefix)) * g)) /\ exists ff_q_pointadd_total_decomp_prefix_summand. f = ff_q_pointadd_total_decomp_prefix_summand * S ((S (ff_i_pointadd_total_decomp_prefix)) * g) + (ff_a_pointadd_total_decomp_prefix))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_partial. ff_h_pointadd_total_decomp_prefix_partial + S (ff_r_pointadd_total_decomp_prefix) = S ((S (ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_partial. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_partial * S ((S (ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix) + (ff_r_pointadd_total_decomp_prefix))) /\ ((((exists ff_h_pointadd_total_decomp_prefix_successor. ff_h_pointadd_total_decomp_prefix_successor + S (ff_s_pointadd_total_decomp_prefix) = S ((S (S ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix)) /\ exists ff_q_pointadd_total_decomp_prefix_successor. ff_u_pointadd_total_decomp_prefix = ff_q_pointadd_total_decomp_prefix_successor * S ((S (S ff_i_pointadd_total_decomp_prefix)) * ff_v_pointadd_total_decomp_prefix) + (ff_s_pointadd_total_decomp_prefix))) /\ ff_s_pointadd_total_decomp_prefix = ff_r_pointadd_total_decomp_prefix + ff_a_pointadd_total_decomp_prefix)))))) /\ q = r + a)
  67. 0067specialize beta_sum_succ_decompose f
  68. 0068specialize beta_sum_succ_decompose g
  69. 0069specialize beta_sum_succ_decompose l
  70. 0070specialize beta_sum_succ_decompose q
  71. 0071apply beta_sum_succ_decompose
  72. 0072exact htotal
  73. 0073cases htotal_decomp
  74. 0074cases htotal_decomp_witness
  75. 0075cases htotal_decomp_witness_witness
  76. 0076cases htotal_decomp_witness_witness_right
  77. 0077have hprefix_pointwise : forall i a z s. (exists h. h + S i = l) -> (((exists ff_h_pointadd_prefix_left_entry. ff_h_pointadd_prefix_left_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pointadd_prefix_left_entry. b = ff_q_pointadd_prefix_left_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_pointadd_prefix_right_entry. ff_h_pointadd_prefix_right_entry + S (z) = S ((S (i)) * e)) /\ exists ff_q_pointadd_prefix_right_entry. d = ff_q_pointadd_prefix_right_entry * S ((S (i)) * e) + (z))) -> (((exists ff_h_pointadd_prefix_total_entry. ff_h_pointadd_prefix_total_entry + S (s) = S ((S (i)) * g)) /\ exists ff_q_pointadd_prefix_total_entry. f = ff_q_pointadd_prefix_total_entry * S ((S (i)) * g) + (s))) -> s = a + z
  78. 0078intro i
  79. 0079intro a
  80. 0080intro z
  81. 0081intro s
  82. 0082intro hi
  83. 0083intro ha
  84. 0084intro hz
  85. 0085intro hs
  86. 0086specialize hpointwise i
  87. 0087specialize hpointwise a
  88. 0088specialize hpointwise z
  89. 0089specialize hpointwise s
  90. 0090apply hpointwise
  91. 0091specialize le_succ (S i)
  92. 0092specialize le_succ l
  93. 0093apply le_succ
  94. 0094exact hi
  95. 0095exact ha
  96. 0096exact hz
  97. 0097exact hs
  98. 0098have hprefix : x1 + x3 = x5
  99. 0099specialize IH x1
  100. 0100specialize IH x3
  101. 0101specialize IH x5
  102. 0102apply IH
  103. 0103exact hleft_decomp_witness_witness_right_left
  104. 0104exact hright_decomp_witness_witness_right_left
  105. 0105exact htotal_decomp_witness_witness_right_left
  106. 0106exact hprefix_pointwise
  107. 0107have hlast : x4 = x + x2
  108. 0108specialize hpointwise l
  109. 0109specialize hpointwise x
  110. 0110specialize hpointwise x2
  111. 0111specialize hpointwise x4
  112. 0112apply hpointwise
  113. 0113specialize le_refl (S l)
  114. 0114exact le_refl
  115. 0115exact hleft_decomp_witness_witness_left
  116. 0116exact hright_decomp_witness_witness_left
  117. 0117exact htotal_decomp_witness_witness_left
  118. 0118rewrite hleft_decomp_witness_witness_right_right
  119. 0119rewrite hright_decomp_witness_witness_right_right
  120. 0120rewrite htotal_decomp_witness_witness_right_right
  121. 0121rewrite hlast
  122. 0122simp [add_assoc, add_comm]
  123. 0123trans (x1 + x3) + (x2 + x)
  124. 0124symm
  125. 0125apply add_assoc
  126. 0126rewrite hprefix
  127. 0127refl