BD0008

binary_length_upper_power_bound

Every actual BitLen witness supplies the exact beta-coded upper power 2^l and the strict inequality n < 2^l, including zero.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ n. ∀ l. BitLen(n,l) → ∃ x. PowTwo(l,x) ∧ Lt(n,x)

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

Definition DAG

PowTwo(e,p) · 1BitLen(n,ell) · 1Lt(a,b) · 1

Actual proof prerequisites

binary_power_two_exists · checked external prerequisitebinary_power_two_nonzero · checked external prerequisiteone_le_of_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall n l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_upper_length ff_lower_bl_bd_upper_length ff_upper_bl_bd_upper_length. (((l) = S ff_exponent_bl_bd_upper_length) /\ ((exists ff_positive_bl_bd_upper_length. ff_positive_bl_bd_upper_length + 1 = (n)) /\ ((exists pa_b_bl_bd_upper_length_lower pa_c_bl_bd_upper_length_lower. ((forall pa_i_bl_bd_upper_length_lower_repeat. (exists pa_lt_bl_bd_upper_length_lower_repeat_bound. pa_lt_bl_bd_upper_length_lower_repeat_bound + S pa_i_bl_bd_upper_length_lower_repeat = ff_exponent_bl_bd_upper_length) -> (((exists pa_h_bl_bd_upper_length_lower_repeat_decoded. pa_h_bl_bd_upper_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_length_lower_repeat)) * pa_c_bl_bd_upper_length_lower)) /\ exists pa_q_bl_bd_upper_length_lower_repeat_decoded. pa_b_bl_bd_upper_length_lower = pa_q_bl_bd_upper_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_upper_length_lower_repeat)) * pa_c_bl_bd_upper_length_lower) + (2)))) /\ (exists pa_u_bl_bd_upper_length_lower_product pa_v_bl_bd_upper_length_lower_product. ((((exists pa_h_bl_bd_upper_length_lower_product_start. pa_h_bl_bd_upper_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_start. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_upper_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_terminal. pa_h_bl_bd_upper_length_lower_product_terminal + S (ff_lower_bl_bd_upper_length) = S ((S (ff_exponent_bl_bd_upper_length)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_terminal. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_upper_length)) * pa_v_bl_bd_upper_length_lower_product) + (ff_lower_bl_bd_upper_length))) /\ forall pa_i_bl_bd_upper_length_lower_product. (exists pa_lt_bl_bd_upper_length_lower_product_bound. pa_lt_bl_bd_upper_length_lower_product_bound + S pa_i_bl_bd_upper_length_lower_product = ff_exponent_bl_bd_upper_length) -> exists pa_p_bl_bd_upper_length_lower_product pa_r_bl_bd_upper_length_lower_product pa_s_bl_bd_upper_length_lower_product. ((((exists pa_h_bl_bd_upper_length_lower_product_factor. pa_h_bl_bd_upper_length_lower_product_factor + S (pa_p_bl_bd_upper_length_lower_product) = S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_c_bl_bd_upper_length_lower)) /\ exists pa_q_bl_bd_upper_length_lower_product_factor. pa_b_bl_bd_upper_length_lower = pa_q_bl_bd_upper_length_lower_product_factor * S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_c_bl_bd_upper_length_lower) + (pa_p_bl_bd_upper_length_lower_product))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_partial. pa_h_bl_bd_upper_length_lower_product_partial + S (pa_r_bl_bd_upper_length_lower_product) = S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_partial. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_partial * S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product) + (pa_r_bl_bd_upper_length_lower_product))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_successor. pa_h_bl_bd_upper_length_lower_product_successor + S (pa_s_bl_bd_upper_length_lower_product) = S ((S (S pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_successor. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_successor * S ((S (S pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product) + (pa_s_bl_bd_upper_length_lower_product))) /\ pa_s_bl_bd_upper_length_lower_product = pa_r_bl_bd_upper_length_lower_product * pa_p_bl_bd_upper_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_upper_length_upper pa_c_bl_bd_upper_length_upper. ((forall pa_i_bl_bd_upper_length_upper_repeat. (exists pa_lt_bl_bd_upper_length_upper_repeat_bound. pa_lt_bl_bd_upper_length_upper_repeat_bound + S pa_i_bl_bd_upper_length_upper_repeat = l) -> (((exists pa_h_bl_bd_upper_length_upper_repeat_decoded. pa_h_bl_bd_upper_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_length_upper_repeat)) * pa_c_bl_bd_upper_length_upper)) /\ exists pa_q_bl_bd_upper_length_upper_repeat_decoded. pa_b_bl_bd_upper_length_upper = pa_q_bl_bd_upper_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_upper_length_upper_repeat)) * pa_c_bl_bd_upper_length_upper) + (2)))) /\ (exists pa_u_bl_bd_upper_length_upper_product pa_v_bl_bd_upper_length_upper_product. ((((exists pa_h_bl_bd_upper_length_upper_product_start. pa_h_bl_bd_upper_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_start. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_upper_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_terminal. pa_h_bl_bd_upper_length_upper_product_terminal + S (ff_upper_bl_bd_upper_length) = S ((S (l)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_terminal. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_upper_length_upper_product) + (ff_upper_bl_bd_upper_length))) /\ forall pa_i_bl_bd_upper_length_upper_product. (exists pa_lt_bl_bd_upper_length_upper_product_bound. pa_lt_bl_bd_upper_length_upper_product_bound + S pa_i_bl_bd_upper_length_upper_product = l) -> exists pa_p_bl_bd_upper_length_upper_product pa_r_bl_bd_upper_length_upper_product pa_s_bl_bd_upper_length_upper_product. ((((exists pa_h_bl_bd_upper_length_upper_product_factor. pa_h_bl_bd_upper_length_upper_product_factor + S (pa_p_bl_bd_upper_length_upper_product) = S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_c_bl_bd_upper_length_upper)) /\ exists pa_q_bl_bd_upper_length_upper_product_factor. pa_b_bl_bd_upper_length_upper = pa_q_bl_bd_upper_length_upper_product_factor * S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_c_bl_bd_upper_length_upper) + (pa_p_bl_bd_upper_length_upper_product))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_partial. pa_h_bl_bd_upper_length_upper_product_partial + S (pa_r_bl_bd_upper_length_upper_product) = S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_partial. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_partial * S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product) + (pa_r_bl_bd_upper_length_upper_product))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_successor. pa_h_bl_bd_upper_length_upper_product_successor + S (pa_s_bl_bd_upper_length_upper_product) = S ((S (S pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_successor. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_successor * S ((S (S pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product) + (pa_s_bl_bd_upper_length_upper_product))) /\ pa_s_bl_bd_upper_length_upper_product = pa_r_bl_bd_upper_length_upper_product * pa_p_bl_bd_upper_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_upper_length. ff_lower_gap_bl_bd_upper_length + (ff_lower_bl_bd_upper_length) = (n)) /\ (exists ff_upper_gap_bl_bd_upper_length. ff_upper_gap_bl_bd_upper_length + S (n) = (ff_upper_bl_bd_upper_length))))))))) -> exists p. ((exists pa_b_bl_bd_upper_power pa_c_bl_bd_upper_power. ((forall pa_i_bl_bd_upper_power_repeat. (exists pa_lt_bl_bd_upper_power_repeat_bound. pa_lt_bl_bd_upper_power_repeat_bound + S pa_i_bl_bd_upper_power_repeat = l) -> (((exists pa_h_bl_bd_upper_power_repeat_decoded. pa_h_bl_bd_upper_power_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_power_repeat)) * pa_c_bl_bd_upper_power)) /\ exists pa_q_bl_bd_upper_power_repeat_decoded. pa_b_bl_bd_upper_power = pa_q_bl_bd_upper_power_repeat_decoded * S ((S (pa_i_bl_bd_upper_power_repeat)) * pa_c_bl_bd_upper_power) + (2)))) /\ (exists pa_u_bl_bd_upper_power_product pa_v_bl_bd_upper_power_product. ((((exists pa_h_bl_bd_upper_power_product_start. pa_h_bl_bd_upper_power_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_start. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_start * S ((S (0)) * pa_v_bl_bd_upper_power_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_power_product_terminal. pa_h_bl_bd_upper_power_product_terminal + S (p) = S ((S (l)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_terminal. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_terminal * S ((S (l)) * pa_v_bl_bd_upper_power_product) + (p))) /\ forall pa_i_bl_bd_upper_power_product. (exists pa_lt_bl_bd_upper_power_product_bound. pa_lt_bl_bd_upper_power_product_bound + S pa_i_bl_bd_upper_power_product = l) -> exists pa_p_bl_bd_upper_power_product pa_r_bl_bd_upper_power_product pa_s_bl_bd_upper_power_product. ((((exists pa_h_bl_bd_upper_power_product_factor. pa_h_bl_bd_upper_power_product_factor + S (pa_p_bl_bd_upper_power_product) = S ((S (pa_i_bl_bd_upper_power_product)) * pa_c_bl_bd_upper_power)) /\ exists pa_q_bl_bd_upper_power_product_factor. pa_b_bl_bd_upper_power = pa_q_bl_bd_upper_power_product_factor * S ((S (pa_i_bl_bd_upper_power_product)) * pa_c_bl_bd_upper_power) + (pa_p_bl_bd_upper_power_product))) /\ ((((exists pa_h_bl_bd_upper_power_product_partial. pa_h_bl_bd_upper_power_product_partial + S (pa_r_bl_bd_upper_power_product) = S ((S (pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_partial. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_partial * S ((S (pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product) + (pa_r_bl_bd_upper_power_product))) /\ ((((exists pa_h_bl_bd_upper_power_product_successor. pa_h_bl_bd_upper_power_product_successor + S (pa_s_bl_bd_upper_power_product) = S ((S (S pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_successor. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_successor * S ((S (S pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product) + (pa_s_bl_bd_upper_power_product))) /\ pa_s_bl_bd_upper_power_product = pa_r_bl_bd_upper_power_product * pa_p_bl_bd_upper_power_product)))))))) /\ (exists gap. gap + S n = p))

Complete unchanged native tactic proof

All 35 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

35 script commands · 13 reading checkpoints · 2 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro l
  3. L3
    intro hlength
02Separate the logical casesL4–5

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

  1. L4
    cases hlength
  2. L5
    cases hlength_left
03Establish hpowerL6–8

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have hpower : ∃ value. PowTwo(l,value)Definitions: PowTwoOriginal native command in the exact edition
  2. L7
    specialize binary_power_two_exists l
  3. L8
    exact binary_power_two_exists
04Separate the logical casesL9–9

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

  1. L9
    cases hpower
05Construct an explicit witnessL10–10

Supply the displayed value, then prove that it has the required property.

  1. L10
    exists x
06Separate the logical casesL11–11

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

  1. L11
    split
07Use earlier factsL12–12

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

  1. L12
    exact hpower_witness
08Establish hnonzeroL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two nonzero.

  1. L13
    have hnonzero : ~(x = 0)
  2. L14
    intro hzero
  3. L15
    specialize binary_power_two_nonzero l
  4. L16
    specialize binary_power_two_nonzero x
  5. L17
    apply binary_power_two_nonzero
  6. L18
    exact hpower_witness
  7. L19
    exact hzero
  8. L20
    rewrite hlength_left_left
  9. L21
    specialize one_le_of_ne_zero x
  10. L22
    apply one_le_of_ne_zero
09Use earlier factsL23–23

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

  1. L23
    exact hnonzero
10Separate the logical casesL24–31

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

  1. L24
    cases hlength_right
  2. L25
    cases hlength_right_witness
  3. L26
    cases hlength_right_witness_witness
  4. L27
    cases hlength_right_witness_witness_witness
  5. L28
    cases hlength_right_witness_witness_witness_right
  6. L29
    cases hlength_right_witness_witness_witness_right_right
  7. L30
    cases hlength_right_witness_witness_witness_right_right_right
  8. L31
    cases hlength_right_witness_witness_witness_right_right_right_right
11Construct an explicit witnessL32–32

Supply the displayed value, then prove that it has the required property.

  1. L32
    exists x2
12Separate the logical casesL33–33

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

  1. L33
    split
13Use earlier factsL34–35

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

  1. L34
    exact hlength_right_witness_witness_witness_right_right_right_left
  2. L35
    exact hlength_right_witness_witness_witness_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro hlength
  4. 0004cases hlength
  5. 0005cases hlength_left
  6. 0006have hpower : exists value. (exists pa_b_bl_bd_zero_upper pa_c_bl_bd_zero_upper. ((forall pa_i_bl_bd_zero_upper_repeat. (exists pa_lt_bl_bd_zero_upper_repeat_bound. pa_lt_bl_bd_zero_upper_repeat_bound + S pa_i_bl_bd_zero_upper_repeat = l) -> (((exists pa_h_bl_bd_zero_upper_repeat_decoded. pa_h_bl_bd_zero_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_zero_upper_repeat)) * pa_c_bl_bd_zero_upper)) /\ exists pa_q_bl_bd_zero_upper_repeat_decoded. pa_b_bl_bd_zero_upper = pa_q_bl_bd_zero_upper_repeat_decoded * S ((S (pa_i_bl_bd_zero_upper_repeat)) * pa_c_bl_bd_zero_upper) + (2)))) /\ (exists pa_u_bl_bd_zero_upper_product pa_v_bl_bd_zero_upper_product. ((((exists pa_h_bl_bd_zero_upper_product_start. pa_h_bl_bd_zero_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_start. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_start * S ((S (0)) * pa_v_bl_bd_zero_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_zero_upper_product_terminal. pa_h_bl_bd_zero_upper_product_terminal + S (value) = S ((S (l)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_terminal. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_zero_upper_product) + (value))) /\ forall pa_i_bl_bd_zero_upper_product. (exists pa_lt_bl_bd_zero_upper_product_bound. pa_lt_bl_bd_zero_upper_product_bound + S pa_i_bl_bd_zero_upper_product = l) -> exists pa_p_bl_bd_zero_upper_product pa_r_bl_bd_zero_upper_product pa_s_bl_bd_zero_upper_product. ((((exists pa_h_bl_bd_zero_upper_product_factor. pa_h_bl_bd_zero_upper_product_factor + S (pa_p_bl_bd_zero_upper_product) = S ((S (pa_i_bl_bd_zero_upper_product)) * pa_c_bl_bd_zero_upper)) /\ exists pa_q_bl_bd_zero_upper_product_factor. pa_b_bl_bd_zero_upper = pa_q_bl_bd_zero_upper_product_factor * S ((S (pa_i_bl_bd_zero_upper_product)) * pa_c_bl_bd_zero_upper) + (pa_p_bl_bd_zero_upper_product))) /\ ((((exists pa_h_bl_bd_zero_upper_product_partial. pa_h_bl_bd_zero_upper_product_partial + S (pa_r_bl_bd_zero_upper_product) = S ((S (pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_partial. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_partial * S ((S (pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product) + (pa_r_bl_bd_zero_upper_product))) /\ ((((exists pa_h_bl_bd_zero_upper_product_successor. pa_h_bl_bd_zero_upper_product_successor + S (pa_s_bl_bd_zero_upper_product) = S ((S (S pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_successor. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_successor * S ((S (S pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product) + (pa_s_bl_bd_zero_upper_product))) /\ pa_s_bl_bd_zero_upper_product = pa_r_bl_bd_zero_upper_product * pa_p_bl_bd_zero_upper_product))))))))
  7. 0007specialize binary_power_two_exists l
  8. 0008exact binary_power_two_exists
  9. 0009cases hpower
  10. 0010exists x
  11. 0011split
  12. 0012exact hpower_witness
  13. 0013have hnonzero : ~(x = 0)
  14. 0014intro hzero
  15. 0015specialize binary_power_two_nonzero l
  16. 0016specialize binary_power_two_nonzero x
  17. 0017apply binary_power_two_nonzero
  18. 0018exact hpower_witness
  19. 0019exact hzero
  20. 0020rewrite hlength_left_left
  21. 0021specialize one_le_of_ne_zero x
  22. 0022apply one_le_of_ne_zero
  23. 0023exact hnonzero
  24. 0024cases hlength_right
  25. 0025cases hlength_right_witness
  26. 0026cases hlength_right_witness_witness
  27. 0027cases hlength_right_witness_witness_witness
  28. 0028cases hlength_right_witness_witness_witness_right
  29. 0029cases hlength_right_witness_witness_witness_right_right
  30. 0030cases hlength_right_witness_witness_witness_right_right_right
  31. 0031cases hlength_right_witness_witness_witness_right_right_right_right
  32. 0032exists x2
  33. 0033split
  34. 0034exact hlength_right_witness_witness_witness_right_right_right_left
  35. 0035exact hlength_right_witness_witness_witness_right_right_right_right_right