PC0014

beta_cutoff_count_comparison

The full bit count is at most the cutoff index plus the actual count above that index.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ u. ∀ b. ∀ c. ∀ d. ∀ f. ∀ l. ∀ k. ∀ L. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 0 ∨ y = 1)) → BetaCutoffPrefix(u,b,c,d,f,l) → Sum(b,c,l,k) → Sum(d,f,l,L) → Le(k,u + L)

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

Definition DAG

BetaCutoffPrefix(u,b,c,d,f,l) · 1Le(a,b) · 5Lt(a,b) · 3BetaAt(b,c,i,x) · 4Sum(b,c,l,z) · 4

Actual proof prerequisites

beta_sum_zero · checked external prerequisitezero_le · checked external prerequisitele_or_lt · checked external prerequisitebit_count_bounded · checked external prerequisitele_trans · checked external prerequisitele_add_right · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitebeta_cutoff_prefix_entryle_refl · checked external prerequisitelt_not_le · checked external prerequisitebeta_at_unique · checked external prerequisiteall_bits_prefix_succ · checked external prerequisitebeta_cutoff_prefix_drop_lastadd_le_add_right · checked external prerequisiteadd_assoc · checked external prerequisite
Original expanded first-order statement 
forall u b c d f l k L. (forall pc_index_cut_count_bits. (exists pc_lt_cut_count_bits_bound. pc_lt_cut_count_bits_bound + S (pc_index_cut_count_bits) = (l)) -> exists pc_bit_cut_count_bits. (((exists fs_h_pc_cut_count_bits_entry. fs_h_pc_cut_count_bits_entry + S (pc_bit_cut_count_bits) = S ((S (pc_index_cut_count_bits)) * c)) /\ exists fs_q_pc_cut_count_bits_entry. b = fs_q_pc_cut_count_bits_entry * S ((S (pc_index_cut_count_bits)) * c) + (pc_bit_cut_count_bits))) /\ (pc_bit_cut_count_bits = 0 \/ pc_bit_cut_count_bits = 1)) -> (forall pc_index_cut_count_source. (exists pc_lt_cut_count_source_bound. pc_lt_cut_count_source_bound + S (pc_index_cut_count_source) = (l)) -> exists pc_bit_cut_count_source. (((exists fs_h_pc_cut_count_source_entry. fs_h_pc_cut_count_source_entry + S (pc_bit_cut_count_source) = S ((S (pc_index_cut_count_source)) * f)) /\ exists fs_q_pc_cut_count_source_entry. d = fs_q_pc_cut_count_source_entry * S ((S (pc_index_cut_count_source)) * f) + (pc_bit_cut_count_source))) /\ ((((exists pc_lt_cut_count_source_choice_below. pc_lt_cut_count_source_choice_below + S (pc_index_cut_count_source) = (u)) /\ pc_bit_cut_count_source = 0) \/ ((exists pc_le_cut_count_source_choice_above. pc_le_cut_count_source_choice_above + (u) = (pc_index_cut_count_source)) /\ (((exists fs_h_pc_cut_count_source_choice_source. fs_h_pc_cut_count_source_choice_source + S (pc_bit_cut_count_source) = S ((S (pc_index_cut_count_source)) * c)) /\ exists fs_q_pc_cut_count_source_choice_source. b = fs_q_pc_cut_count_source_choice_source * S ((S (pc_index_cut_count_source)) * c) + (pc_bit_cut_count_source))))))) -> (exists fs_u_pc_cut_count_whole fs_v_pc_cut_count_whole. ((((exists fs_h_pc_cut_count_whole_body_start. fs_h_pc_cut_count_whole_body_start + S (0) = S ((S (0)) * fs_v_pc_cut_count_whole)) /\ exists fs_q_pc_cut_count_whole_body_start. fs_u_pc_cut_count_whole = fs_q_pc_cut_count_whole_body_start * S ((S (0)) * fs_v_pc_cut_count_whole) + (0))) /\ ((((exists fs_h_pc_cut_count_whole_body_terminal. fs_h_pc_cut_count_whole_body_terminal + S (k) = S ((S (l)) * fs_v_pc_cut_count_whole)) /\ exists fs_q_pc_cut_count_whole_body_terminal. fs_u_pc_cut_count_whole = fs_q_pc_cut_count_whole_body_terminal * S ((S (l)) * fs_v_pc_cut_count_whole) + (k))) /\ forall fs_i_pc_cut_count_whole_body_steps. (exists fs_lt_pc_cut_count_whole_body_steps_bound. fs_lt_pc_cut_count_whole_body_steps_bound + S fs_i_pc_cut_count_whole_body_steps = l) -> exists fs_a_pc_cut_count_whole_body_steps fs_r_pc_cut_count_whole_body_steps fs_s_pc_cut_count_whole_body_steps. ((((exists fs_h_pc_cut_count_whole_body_steps_summand. fs_h_pc_cut_count_whole_body_steps_summand + S (fs_a_pc_cut_count_whole_body_steps) = S ((S (fs_i_pc_cut_count_whole_body_steps)) * c)) /\ exists fs_q_pc_cut_count_whole_body_steps_summand. b = fs_q_pc_cut_count_whole_body_steps_summand * S ((S (fs_i_pc_cut_count_whole_body_steps)) * c) + (fs_a_pc_cut_count_whole_body_steps))) /\ ((((exists fs_h_pc_cut_count_whole_body_steps_partial. fs_h_pc_cut_count_whole_body_steps_partial + S (fs_r_pc_cut_count_whole_body_steps) = S ((S (fs_i_pc_cut_count_whole_body_steps)) * fs_v_pc_cut_count_whole)) /\ exists fs_q_pc_cut_count_whole_body_steps_partial. fs_u_pc_cut_count_whole = fs_q_pc_cut_count_whole_body_steps_partial * S ((S (fs_i_pc_cut_count_whole_body_steps)) * fs_v_pc_cut_count_whole) + (fs_r_pc_cut_count_whole_body_steps))) /\ ((((exists fs_h_pc_cut_count_whole_body_steps_successor. fs_h_pc_cut_count_whole_body_steps_successor + S (fs_s_pc_cut_count_whole_body_steps) = S ((S (S fs_i_pc_cut_count_whole_body_steps)) * fs_v_pc_cut_count_whole)) /\ exists fs_q_pc_cut_count_whole_body_steps_successor. fs_u_pc_cut_count_whole = fs_q_pc_cut_count_whole_body_steps_successor * S ((S (S fs_i_pc_cut_count_whole_body_steps)) * fs_v_pc_cut_count_whole) + (fs_s_pc_cut_count_whole_body_steps))) /\ fs_s_pc_cut_count_whole_body_steps = fs_r_pc_cut_count_whole_body_steps + fs_a_pc_cut_count_whole_body_steps)))))) -> (exists fs_u_pc_cut_count_tail fs_v_pc_cut_count_tail. ((((exists fs_h_pc_cut_count_tail_body_start. fs_h_pc_cut_count_tail_body_start + S (0) = S ((S (0)) * fs_v_pc_cut_count_tail)) /\ exists fs_q_pc_cut_count_tail_body_start. fs_u_pc_cut_count_tail = fs_q_pc_cut_count_tail_body_start * S ((S (0)) * fs_v_pc_cut_count_tail) + (0))) /\ ((((exists fs_h_pc_cut_count_tail_body_terminal. fs_h_pc_cut_count_tail_body_terminal + S (L) = S ((S (l)) * fs_v_pc_cut_count_tail)) /\ exists fs_q_pc_cut_count_tail_body_terminal. fs_u_pc_cut_count_tail = fs_q_pc_cut_count_tail_body_terminal * S ((S (l)) * fs_v_pc_cut_count_tail) + (L))) /\ forall fs_i_pc_cut_count_tail_body_steps. (exists fs_lt_pc_cut_count_tail_body_steps_bound. fs_lt_pc_cut_count_tail_body_steps_bound + S fs_i_pc_cut_count_tail_body_steps = l) -> exists fs_a_pc_cut_count_tail_body_steps fs_r_pc_cut_count_tail_body_steps fs_s_pc_cut_count_tail_body_steps. ((((exists fs_h_pc_cut_count_tail_body_steps_summand. fs_h_pc_cut_count_tail_body_steps_summand + S (fs_a_pc_cut_count_tail_body_steps) = S ((S (fs_i_pc_cut_count_tail_body_steps)) * f)) /\ exists fs_q_pc_cut_count_tail_body_steps_summand. d = fs_q_pc_cut_count_tail_body_steps_summand * S ((S (fs_i_pc_cut_count_tail_body_steps)) * f) + (fs_a_pc_cut_count_tail_body_steps))) /\ ((((exists fs_h_pc_cut_count_tail_body_steps_partial. fs_h_pc_cut_count_tail_body_steps_partial + S (fs_r_pc_cut_count_tail_body_steps) = S ((S (fs_i_pc_cut_count_tail_body_steps)) * fs_v_pc_cut_count_tail)) /\ exists fs_q_pc_cut_count_tail_body_steps_partial. fs_u_pc_cut_count_tail = fs_q_pc_cut_count_tail_body_steps_partial * S ((S (fs_i_pc_cut_count_tail_body_steps)) * fs_v_pc_cut_count_tail) + (fs_r_pc_cut_count_tail_body_steps))) /\ ((((exists fs_h_pc_cut_count_tail_body_steps_successor. fs_h_pc_cut_count_tail_body_steps_successor + S (fs_s_pc_cut_count_tail_body_steps) = S ((S (S fs_i_pc_cut_count_tail_body_steps)) * fs_v_pc_cut_count_tail)) /\ exists fs_q_pc_cut_count_tail_body_steps_successor. fs_u_pc_cut_count_tail = fs_q_pc_cut_count_tail_body_steps_successor * S ((S (S fs_i_pc_cut_count_tail_body_steps)) * fs_v_pc_cut_count_tail) + (fs_s_pc_cut_count_tail_body_steps))) /\ fs_s_pc_cut_count_tail_body_steps = fs_r_pc_cut_count_tail_body_steps + fs_a_pc_cut_count_tail_body_steps)))))) -> (exists pc_le_cut_count_result. pc_le_cut_count_result + (k) = (u + L))

Complete tactic proof in conservative notation

All 141 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

141 script commands · 25 reading checkpoints · 9 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 (2)
beta cutoff prefix entrybeta cutoff prefix drop last
01Fix variables and assumptionsL1–5

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

  1. L1
    intro u
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro f
02Induction on lL6–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction l
  2. L7
    intro k
  3. L8
    intro L
  4. L9
    intro hb
  5. L10
    intro hc
  6. L11
    intro hk
  7. L12
    intro hL
03Establish hk0L13–22

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

  1. L13
    have hk0 : k = 0
  2. L14
    specialize beta_sum_zero b
  3. L15
    specialize beta_sum_zero c
  4. L16
    specialize beta_sum_zero k
  5. L17
    apply beta_sum_zero
  6. L18
    exact hk
  7. L19
    rewrite hk0
  8. L20
    specialize zero_le (u + L)
  9. L21
    apply zero_le
  10. L22
    intro k
04Fix variables and assumptionsL23–27

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

  1. L23
    intro L
  2. L24
    intro hb
  3. L25
    intro hc
  4. L26
    intro hk
  5. L27
    intro hL
05Establish hsL28–31

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

  1. L28
    have hs : Le(u,l) ∨ Lt(l,u)Definitions: Le(u,l)Lt(l,u)Original native command in the exact edition
  2. L29
    specialize le_or_lt u
  3. L30
    specialize le_or_lt l
  4. L31
    apply le_or_lt
06Separate the logical casesL32–32

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

  1. L32
    cases hs
07Establish hdL33–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L33
    have hd : ∃ e. ∃ K. BetaAt(b,c,l,e) ∧ (Sum(b,c,l,K) ∧ k = K + e)Definitions: BetaAt(b,c,l,e)Sum(b,c,l,K)Original native command in the exact edition
  2. L34
    specialize beta_sum_succ_decompose b
  3. L35
    specialize beta_sum_succ_decompose c
  4. L36
    specialize beta_sum_succ_decompose l
  5. L37
    specialize beta_sum_succ_decompose k
  6. L38
    apply beta_sum_succ_decompose
  7. L39
    exact hk
08Separate the logical casesL40–43

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

  1. L40
    cases hd
  2. L41
    cases hd_witness
  3. L42
    cases hd_witness_witness
  4. L43
    cases hd_witness_witness_right
09Establish heL44–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L44
    have he : ∃ e. ∃ M. BetaAt(d,f,l,e) ∧ (Sum(d,f,l,M) ∧ L = M + e)Definitions: BetaAt(d,f,l,e)Sum(d,f,l,M)Original native command in the exact edition
  2. L45
    specialize beta_sum_succ_decompose d
  3. L46
    specialize beta_sum_succ_decompose f
  4. L47
    specialize beta_sum_succ_decompose l
  5. L48
    specialize beta_sum_succ_decompose L
  6. L49
    apply beta_sum_succ_decompose
  7. L50
    exact hL
10Separate the logical casesL51–54

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

  1. L51
    cases he
  2. L52
    cases he_witness
  3. L53
    cases he_witness_witness
  4. L54
    cases he_witness_witness_right
11Establish hlastL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta cutoff prefix entry.

  1. L55
    have hlast : Lt(l,u) ∧ x2 = 0 ∨ Le(u,l) ∧ BetaAt(b,c,l,x2)Definitions: Lt(l,u)Le(u,l)BetaAt(b,c,l,x2)Original native command in the exact edition
  2. L56
    specialize beta_cutoff_prefix_entry u
  3. L57
    specialize beta_cutoff_prefix_entry b
  4. L58
    specialize beta_cutoff_prefix_entry c
  5. L59
    specialize beta_cutoff_prefix_entry d
  6. L60
    specialize beta_cutoff_prefix_entry f
  7. L61
    specialize beta_cutoff_prefix_entry (S l)
  8. L62
    specialize beta_cutoff_prefix_entry l
  9. L63
    specialize beta_cutoff_prefix_entry x2
  10. L64
    apply beta_cutoff_prefix_entry
12Use earlier factsL65–68

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

  1. L65
    exact hc
  2. L66
    specialize le_refl (S l)
  3. L67
    apply le_refl
  4. L68
    exact he_witness_witness_left
13Separate the logical casesL69–71

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

  1. L69
    cases hlast
  2. L70
    cases hlast_left
  3. L71
    exfalso
14Use earlier factsL72–76

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

  1. L72
    specialize lt_not_le l
  2. L73
    specialize lt_not_le u
  3. L74
    apply lt_not_le
  4. L75
    exact hlast_left_left
  5. L76
    exact hs_left
15Separate the logical casesL77–77

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

  1. L77
    cases hlast_right
16Establish heqL78–86

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

  1. L78
    have heq : x = x2
  2. L79
    specialize beta_at_unique b
  3. L80
    specialize beta_at_unique c
  4. L81
    specialize beta_at_unique l
  5. L82
    specialize beta_at_unique x
  6. L83
    specialize beta_at_unique x2
  7. L84
    apply beta_at_unique
  8. L85
    exact hd_witness_witness_left
  9. L86
    exact hlast_right_right
17Establish hpreL87–96

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

  1. L87
    have hpre : Le(x1,u + x3)Definitions: Le(x1,u + x3)Original native command in the exact edition
  2. L88
    specialize IH x1
  3. L89
    specialize IH x3
  4. L90
    apply IH
  5. L91
    specialize all_bits_prefix_succ b
  6. L92
    specialize all_bits_prefix_succ c
  7. L93
    specialize all_bits_prefix_succ l
  8. L94
    specialize all_bits_prefix_succ (S l)
  9. L95
    apply all_bits_prefix_succ
  10. L96
    refl
18Use earlier factsL97–106

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

  1. L97
    exact hb
  2. L98
    specialize beta_cutoff_prefix_drop_last u
  3. L99
    specialize beta_cutoff_prefix_drop_last b
  4. L100
    specialize beta_cutoff_prefix_drop_last c
  5. L101
    specialize beta_cutoff_prefix_drop_last d
  6. L102
    specialize beta_cutoff_prefix_drop_last f
  7. L103
    specialize beta_cutoff_prefix_drop_last l
  8. L104
    apply beta_cutoff_prefix_drop_last
  9. L105
    exact hc
  10. L106
    exact hd_witness_witness_right_left
19Use earlier factsL107–107

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

  1. L107
    exact he_witness_witness_right_left
20Calculate and transport equalitiesL108–110

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

  1. L108
    rewrite hd_witness_witness_right_right
  2. L109
    rewrite he_witness_witness_right_right
  3. L110
    rewrite heq
21Establish hassocL111–119

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

  1. L111
    have hassoc : u + (x3 + x2) = (u + x3) + x2
  2. L112
    symm
  3. L113
    apply add_assoc
  4. L114
    rewrite hassoc
  5. L115
    specialize add_le_add_right x1
  6. L116
    specialize add_le_add_right (u + x3)
  7. L117
    specialize add_le_add_right x2
  8. L118
    apply add_le_add_right
  9. L119
    exact hpre
22Establish hsmallL120–129

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

  1. L120
    have hsmall : Le(k,u)Definitions: Le(k,u)Original native command in the exact edition
  2. L121
    specialize le_trans k
  3. L122
    specialize le_trans (S l)
  4. L123
    specialize le_trans u
  5. L124
    apply le_trans
  6. L125
    specialize bit_count_bounded b
  7. L126
    specialize bit_count_bounded c
  8. L127
    specialize bit_count_bounded (S l)
  9. L128
    specialize bit_count_bounded k
  10. L129
    apply bit_count_bounded
23Separate the logical casesL130–130

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

  1. L130
    split
24Use earlier factsL131–140

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

  1. L131
    exact hk
  2. L132
    exact hb
  3. L133
    exact hs_right
  4. L134
    specialize le_trans k
  5. L135
    specialize le_trans u
  6. L136
    specialize le_trans (u + L)
  7. L137
    apply le_trans
  8. L138
    exact hsmall
  9. L139
    specialize le_add_right u
  10. L140
    specialize le_add_right L
25Use earlier factsL141–141

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

  1. L141
    apply le_add_right

Library-wide reading audit

Original defined command ledger · 141 lines
  1. 0001intro u
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro f
  6. 0006induction l
  7. 0007intro k
  8. 0008intro L
  9. 0009intro hb
  10. 0010intro hc
  11. 0011intro hk
  12. 0012intro hL
  13. 0013have hk0 : k = 0
  14. 0014specialize beta_sum_zero b
  15. 0015specialize beta_sum_zero c
  16. 0016specialize beta_sum_zero k
  17. 0017apply beta_sum_zero
  18. 0018exact hk
  19. 0019rewrite hk0
  20. 0020specialize zero_le (u + L)
  21. 0021apply zero_le
  22. 0022intro k
  23. 0023intro L
  24. 0024intro hb
  25. 0025intro hc
  26. 0026intro hk
  27. 0027intro hL
  28. 0028have hs : Le(u,l) ∨ Lt(l,u)
  29. 0029specialize le_or_lt u
  30. 0030specialize le_or_lt l
  31. 0031apply le_or_lt
  32. 0032cases hs
  33. 0033have hd : ∃ e. ∃ K. BetaAt(b,c,l,e) ∧ (Sum(b,c,l,K) ∧ k = K + e)
  34. 0034specialize beta_sum_succ_decompose b
  35. 0035specialize beta_sum_succ_decompose c
  36. 0036specialize beta_sum_succ_decompose l
  37. 0037specialize beta_sum_succ_decompose k
  38. 0038apply beta_sum_succ_decompose
  39. 0039exact hk
  40. 0040cases hd
  41. 0041cases hd_witness
  42. 0042cases hd_witness_witness
  43. 0043cases hd_witness_witness_right
  44. 0044have he : ∃ e. ∃ M. BetaAt(d,f,l,e) ∧ (Sum(d,f,l,M) ∧ L = M + e)
  45. 0045specialize beta_sum_succ_decompose d
  46. 0046specialize beta_sum_succ_decompose f
  47. 0047specialize beta_sum_succ_decompose l
  48. 0048specialize beta_sum_succ_decompose L
  49. 0049apply beta_sum_succ_decompose
  50. 0050exact hL
  51. 0051cases he
  52. 0052cases he_witness
  53. 0053cases he_witness_witness
  54. 0054cases he_witness_witness_right
  55. 0055have hlast : Lt(l,u) ∧ x2 = 0 ∨ Le(u,l) ∧ BetaAt(b,c,l,x2)
  56. 0056specialize beta_cutoff_prefix_entry u
  57. 0057specialize beta_cutoff_prefix_entry b
  58. 0058specialize beta_cutoff_prefix_entry c
  59. 0059specialize beta_cutoff_prefix_entry d
  60. 0060specialize beta_cutoff_prefix_entry f
  61. 0061specialize beta_cutoff_prefix_entry (S l)
  62. 0062specialize beta_cutoff_prefix_entry l
  63. 0063specialize beta_cutoff_prefix_entry x2
  64. 0064apply beta_cutoff_prefix_entry
  65. 0065exact hc
  66. 0066specialize le_refl (S l)
  67. 0067apply le_refl
  68. 0068exact he_witness_witness_left
  69. 0069cases hlast
  70. 0070cases hlast_left
  71. 0071exfalso
  72. 0072specialize lt_not_le l
  73. 0073specialize lt_not_le u
  74. 0074apply lt_not_le
  75. 0075exact hlast_left_left
  76. 0076exact hs_left
  77. 0077cases hlast_right
  78. 0078have heq : x = x2
  79. 0079specialize beta_at_unique b
  80. 0080specialize beta_at_unique c
  81. 0081specialize beta_at_unique l
  82. 0082specialize beta_at_unique x
  83. 0083specialize beta_at_unique x2
  84. 0084apply beta_at_unique
  85. 0085exact hd_witness_witness_left
  86. 0086exact hlast_right_right
  87. 0087have hpre : Le(x1,u + x3)
  88. 0088specialize IH x1
  89. 0089specialize IH x3
  90. 0090apply IH
  91. 0091specialize all_bits_prefix_succ b
  92. 0092specialize all_bits_prefix_succ c
  93. 0093specialize all_bits_prefix_succ l
  94. 0094specialize all_bits_prefix_succ (S l)
  95. 0095apply all_bits_prefix_succ
  96. 0096refl
  97. 0097exact hb
  98. 0098specialize beta_cutoff_prefix_drop_last u
  99. 0099specialize beta_cutoff_prefix_drop_last b
  100. 0100specialize beta_cutoff_prefix_drop_last c
  101. 0101specialize beta_cutoff_prefix_drop_last d
  102. 0102specialize beta_cutoff_prefix_drop_last f
  103. 0103specialize beta_cutoff_prefix_drop_last l
  104. 0104apply beta_cutoff_prefix_drop_last
  105. 0105exact hc
  106. 0106exact hd_witness_witness_right_left
  107. 0107exact he_witness_witness_right_left
  108. 0108rewrite hd_witness_witness_right_right
  109. 0109rewrite he_witness_witness_right_right
  110. 0110rewrite heq
  111. 0111have hassoc : u + (x3 + x2) = (u + x3) + x2
  112. 0112symm
  113. 0113apply add_assoc
  114. 0114rewrite hassoc
  115. 0115specialize add_le_add_right x1
  116. 0116specialize add_le_add_right (u + x3)
  117. 0117specialize add_le_add_right x2
  118. 0118apply add_le_add_right
  119. 0119exact hpre
  120. 0120have hsmall : Le(k,u)
  121. 0121specialize le_trans k
  122. 0122specialize le_trans (S l)
  123. 0123specialize le_trans u
  124. 0124apply le_trans
  125. 0125specialize bit_count_bounded b
  126. 0126specialize bit_count_bounded c
  127. 0127specialize bit_count_bounded (S l)
  128. 0128specialize bit_count_bounded k
  129. 0129apply bit_count_bounded
  130. 0130split
  131. 0131exact hk
  132. 0132exact hb
  133. 0133exact hs_right
  134. 0134specialize le_trans k
  135. 0135specialize le_trans u
  136. 0136specialize le_trans (u + L)
  137. 0137apply le_trans
  138. 0138exact hsmall
  139. 0139specialize le_add_right u
  140. 0140specialize le_add_right L
  141. 0141apply le_add_right