power_quotient_prefix_sum_extend_zero

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

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

1. 0001intro p
2. 0002intro n
3. 0003intro b
4. 0004intro c
5. 0005induction g
6. 0006intro t
7. 0007intro e
8. 0008intro hp
9. 0009intro hprefix
10. 0010intro hsum
11. 0011intro hlegendre
12. 0012have hbase_length : n + 0 = n
13. 0013apply PA3
14. 0014rewrite hbase_length at hprefix
15. 0015rewrite hbase_length at hsum
16. 0016rewrite hbase_length at hsum
17. 0017rewrite hbase_length at hsum
18. 0018have hcompeting : exists bls_code_b5cvpsez_base bls_scale_b5cvpsez_base. ((forall bls_index_b5cvpsez_base_prefix. (exists bls_gap_b5cvpsez_base_prefix_bound. bls_gap_b5cvpsez_base_prefix_bound + S (bls_index_b5cvpsez_base_prefix) = (n)) -> exists bls_power_b5cvpsez_base_prefix bls_quotient_b5cvpsez_base_prefix bls_remainder_b5cvpsez_base_prefix. ((exists bpvi_b_bls_b5cvpsez_base_prefix_power bpvi_c_bls_b5cvpsez_base_prefix_power. ((forall bpvi_i_bls_b5cvpsez_base_prefix_power. (exists bpvi_repeat_gap_bls_b5cvpsez_base_prefix_power. bpvi_repeat_gap_bls_b5cvpsez_base_prefix_power + S bpvi_i_bls_b5cvpsez_base_prefix_power = S bls_index_b5cvpsez_base_prefix) -> (((exists bpvi_h_bls_b5cvpsez_base_prefix_power_repeat. bpvi_h_bls_b5cvpsez_base_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_repeat. bpvi_b_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_base_prefix_power bpvi_v_bls_b5cvpsez_base_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_start. bpvi_h_bls_b5cvpsez_base_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_start. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_terminal. bpvi_h_bls_b5cvpsez_base_prefix_power_terminal + S (bls_power_b5cvpsez_base_prefix) = S ((S (S bls_index_b5cvpsez_base_prefix)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_terminal. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_terminal * S ((S (S bls_index_b5cvpsez_base_prefix)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bls_power_b5cvpsez_base_prefix))) /\ forall bpvi_j_bls_b5cvpsez_base_prefix_power. (exists bpvi_product_gap_bls_b5cvpsez_base_prefix_power. bpvi_product_gap_bls_b5cvpsez_base_prefix_power + S bpvi_j_bls_b5cvpsez_base_prefix_power = S bls_index_b5cvpsez_base_prefix) -> exists bpvi_factor_bls_b5cvpsez_base_prefix_power bpvi_partial_bls_b5cvpsez_base_prefix_power bpvi_successor_bls_b5cvpsez_base_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_factor. bpvi_h_bls_b5cvpsez_base_prefix_power_factor + S (bpvi_factor_bls_b5cvpsez_base_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_factor. bpvi_b_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_factor * S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power) + (bpvi_factor_bls_b5cvpsez_base_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_partial. bpvi_h_bls_b5cvpsez_base_prefix_power_partial + S (bpvi_partial_bls_b5cvpsez_base_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_partial. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_partial * S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bpvi_partial_bls_b5cvpsez_base_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_successor. bpvi_h_bls_b5cvpsez_base_prefix_power_successor + S (bpvi_successor_bls_b5cvpsez_base_prefix_power) = S ((S (S bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_successor. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bpvi_successor_bls_b5cvpsez_base_prefix_power))) /\ bpvi_successor_bls_b5cvpsez_base_prefix_power = bpvi_partial_bls_b5cvpsez_base_prefix_power * bpvi_factor_bls_b5cvpsez_base_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_base_prefix_quotient_entry. ff_h_bls_b5cvpsez_base_prefix_quotient_entry + S (bls_quotient_b5cvpsez_base_prefix) = S ((S (bls_index_b5cvpsez_base_prefix)) * bls_scale_b5cvpsez_base)) /\ exists ff_q_bls_b5cvpsez_base_prefix_quotient_entry. bls_code_b5cvpsez_base = ff_q_bls_b5cvpsez_base_prefix_quotient_entry * S ((S (bls_index_b5cvpsez_base_prefix)) * bls_scale_b5cvpsez_base) + (bls_quotient_b5cvpsez_base_prefix))) /\ ((n = bls_power_b5cvpsez_base_prefix * bls_quotient_b5cvpsez_base_prefix + bls_remainder_b5cvpsez_base_prefix /\ exists bls_remainder_gap_b5cvpsez_base_prefix_division. bls_remainder_gap_b5cvpsez_base_prefix_division + S (bls_remainder_b5cvpsez_base_prefix) = bls_power_b5cvpsez_base_prefix))))) /\ (exists ff_u_bls_b5cvpsez_base_sum ff_v_bls_b5cvpsez_base_sum. ((((exists ff_h_bls_b5cvpsez_base_sum_start. ff_h_bls_b5cvpsez_base_sum_start + S (0) = S ((S (0)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_start. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_start * S ((S (0)) * ff_v_bls_b5cvpsez_base_sum) + (0))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_terminal. ff_h_bls_b5cvpsez_base_sum_terminal + S (t) = S ((S (n)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_terminal. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_terminal * S ((S (n)) * ff_v_bls_b5cvpsez_base_sum) + (t))) /\ forall ff_i_bls_b5cvpsez_base_sum. (exists ff_lt_bls_b5cvpsez_base_sum_bound. ff_lt_bls_b5cvpsez_base_sum_bound + S ff_i_bls_b5cvpsez_base_sum = n) -> exists ff_a_bls_b5cvpsez_base_sum ff_r_bls_b5cvpsez_base_sum ff_s_bls_b5cvpsez_base_sum. ((((exists ff_h_bls_b5cvpsez_base_sum_summand. ff_h_bls_b5cvpsez_base_sum_summand + S (ff_a_bls_b5cvpsez_base_sum) = S ((S (ff_i_bls_b5cvpsez_base_sum)) * bls_scale_b5cvpsez_base)) /\ exists ff_q_bls_b5cvpsez_base_sum_summand. bls_code_b5cvpsez_base = ff_q_bls_b5cvpsez_base_sum_summand * S ((S (ff_i_bls_b5cvpsez_base_sum)) * bls_scale_b5cvpsez_base) + (ff_a_bls_b5cvpsez_base_sum))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_partial. ff_h_bls_b5cvpsez_base_sum_partial + S (ff_r_bls_b5cvpsez_base_sum) = S ((S (ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_partial. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_partial * S ((S (ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum) + (ff_r_bls_b5cvpsez_base_sum))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_successor. ff_h_bls_b5cvpsez_base_sum_successor + S (ff_s_bls_b5cvpsez_base_sum) = S ((S (S ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_successor. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_successor * S ((S (S ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum) + (ff_s_bls_b5cvpsez_base_sum))) /\ ff_s_bls_b5cvpsez_base_sum = ff_r_bls_b5cvpsez_base_sum + ff_a_bls_b5cvpsez_base_sum)))))))
19. 0019exists b
20. 0020exists c
21. 0021split
22. 0022exact hprefix
23. 0023exact hsum
24. 0024specialize legendre_sum_functional p
25. 0025specialize legendre_sum_functional n
26. 0026specialize legendre_sum_functional t
27. 0027specialize legendre_sum_functional e
28. 0028apply legendre_sum_functional
29. 0029exact hcompeting
30. 0030exact hlegendre
31. 0031intro t
32. 0032intro e
33. 0033intro hp
34. 0034intro hprefix
35. 0035intro hsum
36. 0036intro hlegendre
37. 0037have hstep_length : n + S g = S (n + g)
38. 0038apply PA4
39. 0039have hrestricted : forall bls_index_b5cvpsez_restricted. (exists bls_gap_b5cvpsez_restricted_bound. bls_gap_b5cvpsez_restricted_bound + S (bls_index_b5cvpsez_restricted) = (n + g)) -> exists bls_power_b5cvpsez_restricted bls_quotient_b5cvpsez_restricted bls_remainder_b5cvpsez_restricted. ((exists bpvi_b_bls_b5cvpsez_restricted_power bpvi_c_bls_b5cvpsez_restricted_power. ((forall bpvi_i_bls_b5cvpsez_restricted_power. (exists bpvi_repeat_gap_bls_b5cvpsez_restricted_power. bpvi_repeat_gap_bls_b5cvpsez_restricted_power + S bpvi_i_bls_b5cvpsez_restricted_power = S bls_index_b5cvpsez_restricted) -> (((exists bpvi_h_bls_b5cvpsez_restricted_power_repeat. bpvi_h_bls_b5cvpsez_restricted_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_repeat. bpvi_b_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_restricted_power bpvi_v_bls_b5cvpsez_restricted_power. ((((exists bpvi_h_bls_b5cvpsez_restricted_power_start. bpvi_h_bls_b5cvpsez_restricted_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_start. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_restricted_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_terminal. bpvi_h_bls_b5cvpsez_restricted_power_terminal + S (bls_power_b5cvpsez_restricted) = S ((S (S bls_index_b5cvpsez_restricted)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_terminal. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_terminal * S ((S (S bls_index_b5cvpsez_restricted)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bls_power_b5cvpsez_restricted))) /\ forall bpvi_j_bls_b5cvpsez_restricted_power. (exists bpvi_product_gap_bls_b5cvpsez_restricted_power. bpvi_product_gap_bls_b5cvpsez_restricted_power + S bpvi_j_bls_b5cvpsez_restricted_power = S bls_index_b5cvpsez_restricted) -> exists bpvi_factor_bls_b5cvpsez_restricted_power bpvi_partial_bls_b5cvpsez_restricted_power bpvi_successor_bls_b5cvpsez_restricted_power. ((((exists bpvi_h_bls_b5cvpsez_restricted_power_factor. bpvi_h_bls_b5cvpsez_restricted_power_factor + S (bpvi_factor_bls_b5cvpsez_restricted_power) = S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_factor. bpvi_b_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_factor * S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power) + (bpvi_factor_bls_b5cvpsez_restricted_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_partial. bpvi_h_bls_b5cvpsez_restricted_power_partial + S (bpvi_partial_bls_b5cvpsez_restricted_power) = S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_partial. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_partial * S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bpvi_partial_bls_b5cvpsez_restricted_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_successor. bpvi_h_bls_b5cvpsez_restricted_power_successor + S (bpvi_successor_bls_b5cvpsez_restricted_power) = S ((S (S bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_successor. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bpvi_successor_bls_b5cvpsez_restricted_power))) /\ bpvi_successor_bls_b5cvpsez_restricted_power = bpvi_partial_bls_b5cvpsez_restricted_power * bpvi_factor_bls_b5cvpsez_restricted_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_restricted_quotient_entry. ff_h_bls_b5cvpsez_restricted_quotient_entry + S (bls_quotient_b5cvpsez_restricted) = S ((S (bls_index_b5cvpsez_restricted)) * c)) /\ exists ff_q_bls_b5cvpsez_restricted_quotient_entry. b = ff_q_bls_b5cvpsez_restricted_quotient_entry * S ((S (bls_index_b5cvpsez_restricted)) * c) + (bls_quotient_b5cvpsez_restricted))) /\ ((n = bls_power_b5cvpsez_restricted * bls_quotient_b5cvpsez_restricted + bls_remainder_b5cvpsez_restricted /\ exists bls_remainder_gap_b5cvpsez_restricted_division. bls_remainder_gap_b5cvpsez_restricted_division + S (bls_remainder_b5cvpsez_restricted) = bls_power_b5cvpsez_restricted))))
40. 0040intro i
41. 0041intro hi
42. 0042specialize hprefix i
43. 0043apply hprefix
44. 0044rewrite hstep_length
45. 0045specialize le_succ (S i)
46. 0046specialize le_succ (n + g)
47. 0047apply le_succ
48. 0048exact hi
49. 0049have htail_start : exists k. k + n = n + g
50. 0050exists g
51. 0051apply add_comm
52. 0052have htail_bound : exists k. k + S (n + g) = n + S g
53. 0053exists 0
54. 0054rewrite hstep_length
55. 0055specialize zero_add (S (n + g))
56. 0056exact zero_add
57. 0057have hzero : ((exists fs_h_b5cvpsez_zero. fs_h_b5cvpsez_zero + S (0) = S ((S (n + g)) * c)) /\ exists fs_q_b5cvpsez_zero. b = fs_q_b5cvpsez_zero * S ((S (n + g)) * c) + (0))
58. 0058specialize power_quotient_prefix_tail_entry_zero p
59. 0059specialize power_quotient_prefix_tail_entry_zero n
60. 0060specialize power_quotient_prefix_tail_entry_zero b
61. 0061specialize power_quotient_prefix_tail_entry_zero c
62. 0062specialize power_quotient_prefix_tail_entry_zero (n + S g)
63. 0063specialize power_quotient_prefix_tail_entry_zero (n + g)
64. 0064apply power_quotient_prefix_tail_entry_zero
65. 0065exact hp
66. 0066exact hprefix
67. 0067exact htail_start
68. 0068exact htail_bound
69. 0069rewrite hstep_length at hsum
70. 0070rewrite hstep_length at hsum
71. 0071rewrite hstep_length at hsum
72. 0072have hprefix_sum : exists fs_u_b5cvpsez_prefix_sum fs_v_b5cvpsez_prefix_sum. ((((exists fs_h_b5cvpsez_prefix_sum_body_start. fs_h_b5cvpsez_prefix_sum_body_start + S (0) = S ((S (0)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_start. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_start * S ((S (0)) * fs_v_b5cvpsez_prefix_sum) + (0))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_terminal. fs_h_b5cvpsez_prefix_sum_body_terminal + S (t) = S ((S (n + g)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_terminal. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_terminal * S ((S (n + g)) * fs_v_b5cvpsez_prefix_sum) + (t))) /\ forall fs_i_b5cvpsez_prefix_sum_body_steps. (exists fs_lt_b5cvpsez_prefix_sum_body_steps_bound. fs_lt_b5cvpsez_prefix_sum_body_steps_bound + S fs_i_b5cvpsez_prefix_sum_body_steps = n + g) -> exists fs_a_b5cvpsez_prefix_sum_body_steps fs_r_b5cvpsez_prefix_sum_body_steps fs_s_b5cvpsez_prefix_sum_body_steps. ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_summand. fs_h_b5cvpsez_prefix_sum_body_steps_summand + S (fs_a_b5cvpsez_prefix_sum_body_steps) = S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * c)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_summand. b = fs_q_b5cvpsez_prefix_sum_body_steps_summand * S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * c) + (fs_a_b5cvpsez_prefix_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_partial. fs_h_b5cvpsez_prefix_sum_body_steps_partial + S (fs_r_b5cvpsez_prefix_sum_body_steps) = S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_partial. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_steps_partial * S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum) + (fs_r_b5cvpsez_prefix_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_successor. fs_h_b5cvpsez_prefix_sum_body_steps_successor + S (fs_s_b5cvpsez_prefix_sum_body_steps) = S ((S (S fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_successor. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_steps_successor * S ((S (S fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum) + (fs_s_b5cvpsez_prefix_sum_body_steps))) /\ fs_s_b5cvpsez_prefix_sum_body_steps = fs_r_b5cvpsez_prefix_sum_body_steps + fs_a_b5cvpsez_prefix_sum_body_steps)))))
73. 0073specialize beta_sum_succ_last_zero b
74. 0074specialize beta_sum_succ_last_zero c
75. 0075specialize beta_sum_succ_last_zero (n + g)
76. 0076specialize beta_sum_succ_last_zero t
77. 0077apply beta_sum_succ_last_zero
78. 0078exact hsum
79. 0079exact hzero
80. 0080specialize IH t
81. 0081specialize IH e
82. 0082apply IH
83. 0083exact hp
84. 0084exact hrestricted
85. 0085exact hprefix_sum
86. 0086exact hlegendre