BT00TM · Bertrand theorem

choose_positive

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every in-range relational Choose value is a successor.

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.

Statement with defined notation

∀ n. ∀ k. ∀ z. Le(k,n) → Choose(n,k,z) → ∃ x. z = S x

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0041 Choose

2 occurrences

In local proof propositions

PD0041 Choose

2 occurrences

Exact expanded native-PA statement
forall n k z. (exists bcf_le_gap_bcp_bound. bcf_le_gap_bcp_bound + (k) = n) -> (((exists bcf_lt_gap_bcp_source_out_of_range. bcf_lt_gap_bcp_source_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bcp_source_in_range. bcf_le_gap_bcp_source_in_range + (k) = n) /\ (exists bcf_row_code_code_bcp_source bcf_row_code_scale_bcp_source bcf_row_scale_code_bcp_source bcf_row_scale_scale_bcp_source bcf_row_code_bcp_source bcf_row_scale_bcp_source. ((forall bcf_row_index_bcp_source_table. (exists bcf_lt_gap_bcp_source_table_row_bound. bcf_lt_gap_bcp_source_table_row_bound + S (bcf_row_index_bcp_source_table) = S (n)) -> exists bcf_row_code_bcp_source_table bcf_row_scale_bcp_source_table. ((((exists bcf_height_bcp_source_table_decoded_row_code. bcf_height_bcp_source_table_decoded_row_code + S (bcf_row_code_bcp_source_table) = S ((S (bcf_row_index_bcp_source_table)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_row_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_table_decoded_row_code * S ((S (bcf_row_index_bcp_source_table)) * bcf_row_code_scale_bcp_source) + (bcf_row_code_bcp_source_table))) /\ ((((exists bcf_height_bcp_source_table_decoded_row_scale. bcf_height_bcp_source_table_decoded_row_scale + S (bcf_row_scale_bcp_source_table) = S ((S (bcf_row_index_bcp_source_table)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_row_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_table_decoded_row_scale * S ((S (bcf_row_index_bcp_source_table)) * bcf_row_scale_scale_bcp_source) + (bcf_row_scale_bcp_source_table))) /\ ((bcf_row_index_bcp_source_table = 0 /\ (forall bcf_index_bcp_source_table_zero_row. (exists bcf_lt_gap_bcp_source_table_zero_row_bound. bcf_lt_gap_bcp_source_table_zero_row_bound + S (bcf_index_bcp_source_table_zero_row) = S (n)) -> exists bcf_value_bcp_source_table_zero_row. ((((exists bcf_height_bcp_source_table_zero_row_entry. bcf_height_bcp_source_table_zero_row_entry + S (bcf_value_bcp_source_table_zero_row) = S ((S (bcf_index_bcp_source_table_zero_row)) * bcf_row_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_zero_row_entry. bcf_row_code_bcp_source_table = bcf_quotient_bcp_source_table_zero_row_entry * S ((S (bcf_index_bcp_source_table_zero_row)) * bcf_row_scale_bcp_source_table) + (bcf_value_bcp_source_table_zero_row))) /\ ((bcf_index_bcp_source_table_zero_row = 0 /\ bcf_value_bcp_source_table_zero_row = 1) \/ exists bcf_predecessor_bcp_source_table_zero_row. bcf_index_bcp_source_table_zero_row = S bcf_predecessor_bcp_source_table_zero_row /\ bcf_value_bcp_source_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_source_table bcf_previous_code_bcp_source_table bcf_previous_scale_bcp_source_table. bcf_row_index_bcp_source_table = S bcf_predecessor_bcp_source_table /\ ((((exists bcf_height_bcp_source_table_decoded_previous_code. bcf_height_bcp_source_table_decoded_previous_code + S (bcf_previous_code_bcp_source_table) = S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_previous_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_code_scale_bcp_source) + (bcf_previous_code_bcp_source_table))) /\ ((((exists bcf_height_bcp_source_table_decoded_previous_scale. bcf_height_bcp_source_table_decoded_previous_scale + S (bcf_previous_scale_bcp_source_table) = S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_table_decoded_previous_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_source_table)) * bcf_row_scale_scale_bcp_source) + (bcf_previous_scale_bcp_source_table))) /\ (forall bcf_index_bcp_source_table_row_step. (exists bcf_lt_gap_bcp_source_table_row_step_bound. bcf_lt_gap_bcp_source_table_row_step_bound + S (bcf_index_bcp_source_table_row_step) = S (n)) -> exists bcf_value_bcp_source_table_row_step. ((((exists bcf_height_bcp_source_table_row_step_entry. bcf_height_bcp_source_table_row_step_entry + S (bcf_value_bcp_source_table_row_step) = S ((S (bcf_index_bcp_source_table_row_step)) * bcf_row_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_entry. bcf_row_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_entry * S ((S (bcf_index_bcp_source_table_row_step)) * bcf_row_scale_bcp_source_table) + (bcf_value_bcp_source_table_row_step))) /\ ((bcf_index_bcp_source_table_row_step = 0 /\ bcf_value_bcp_source_table_row_step = 1) \/ exists bcf_predecessor_bcp_source_table_row_step bcf_left_bcp_source_table_row_step bcf_right_bcp_source_table_row_step. bcf_index_bcp_source_table_row_step = S bcf_predecessor_bcp_source_table_row_step /\ ((((exists bcf_height_bcp_source_table_row_step_previous_left. bcf_height_bcp_source_table_row_step_previous_left + S (bcf_left_bcp_source_table_row_step) = S ((S (bcf_predecessor_bcp_source_table_row_step)) * bcf_previous_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_previous_left. bcf_previous_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_source_table_row_step)) * bcf_previous_scale_bcp_source_table) + (bcf_left_bcp_source_table_row_step))) /\ ((((exists bcf_height_bcp_source_table_row_step_previous_right. bcf_height_bcp_source_table_row_step_previous_right + S (bcf_right_bcp_source_table_row_step) = S ((S (S (bcf_predecessor_bcp_source_table_row_step))) * bcf_previous_scale_bcp_source_table)) /\ exists bcf_quotient_bcp_source_table_row_step_previous_right. bcf_previous_code_bcp_source_table = bcf_quotient_bcp_source_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_source_table_row_step))) * bcf_previous_scale_bcp_source_table) + (bcf_right_bcp_source_table_row_step))) /\ bcf_value_bcp_source_table_row_step = bcf_left_bcp_source_table_row_step + bcf_right_bcp_source_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_source_decoded_row_code. bcf_height_bcp_source_decoded_row_code + S (bcf_row_code_bcp_source) = S ((S (n)) * bcf_row_code_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_row_code. bcf_row_code_code_bcp_source = bcf_quotient_bcp_source_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_source) + (bcf_row_code_bcp_source))) /\ ((((exists bcf_height_bcp_source_decoded_row_scale. bcf_height_bcp_source_decoded_row_scale + S (bcf_row_scale_bcp_source) = S ((S (n)) * bcf_row_scale_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_row_scale. bcf_row_scale_code_bcp_source = bcf_quotient_bcp_source_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_source) + (bcf_row_scale_bcp_source))) /\ (((exists bcf_height_bcp_source_decoded_value. bcf_height_bcp_source_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bcp_source)) /\ exists bcf_quotient_bcp_source_decoded_value. bcf_row_code_bcp_source = bcf_quotient_bcp_source_decoded_value * S ((S (k)) * bcf_row_scale_bcp_source) + (z))))))))) -> exists p. z = S p

Proof neighborhood

Direct theorem prerequisites

BT000Y le_zero BT0017 le_of_succ_le_succ BT0001 add_succ_left BT00T8 choose_exists BT00TE choose_zero BT00TJ choose_succ_succ

Direct theorem dependents

BT00TP central_binom_positive BT00VJ primorial_odd_interval_le_middle

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

69 script commands · 24 reading checkpoints · 5 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 (6)
le zerole of succ le succadd succ leftchoose existschoose zerochoose succ succ
01Induction on nL1–1

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

  1. L1
    induction n
02Induction on kL2–5

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

  1. L2
    induction k
  2. L3
    intro z
  3. L4
    intro hbound
  4. L5
    intro hchoose
03Construct an explicit witnessL6–6

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

  1. L6
    exists 0
04Use earlier factsL7–10

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

  1. L7
    specialize choose_zero 0
  2. L8
    specialize choose_zero z
  3. L9
    apply choose_zero
  4. L10
    exact hchoose
05Fix variables and assumptionsL11–13

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

  1. L11
    intro z
  2. L12
    intro hbound
  3. L13
    intro hchoose
06Establish hk0L14–17

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

  1. L14
    have hk0 : S k = 0
  2. L15
    specialize le_zero (S k)
  3. L16
    apply le_zero
  4. L17
    exact hbound
07Separate the logical casesL18–18

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

  1. L18
    exfalso
08Use earlier factsL19–20

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

  1. L19
    apply PA1
  2. L20
    exact hk0
09Induction on kL21–24

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

  1. L21
    induction k
  2. L22
    intro z
  3. L23
    intro hbound
  4. L24
    intro hchoose
10Construct an explicit witnessL25–25

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

  1. L25
    exists 0
11Use earlier factsL26–29

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

  1. L26
    specialize choose_zero (S n)
  2. L27
    specialize choose_zero z
  3. L28
    apply choose_zero
  4. L29
    exact hchoose
12Fix variables and assumptionsL30–32

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

  1. L30
    intro z
  2. L31
    intro hbound
  3. L32
    intro hchoose
13Establish ha_existsL33–36

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

  1. L33
    have ha_exists : ∃ a. Choose(n,k,a)Definitions: Choose(n,k,a)Original native command in the exact edition
  2. L34
    specialize choose_exists n
  3. L35
    specialize choose_exists k
  4. L36
    exact choose_exists
14Separate the logical casesL37–37

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

  1. L37
    cases ha_exists
15Establish hb_existsL38–41

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

  1. L38
    have hb_exists : ∃ b. Choose(n,S k,b)Definitions: Choose(n,S k,b)Original native command in the exact edition
  2. L39
    specialize choose_exists n
  3. L40
    specialize choose_exists (S k)
  4. L41
    exact choose_exists
16Separate the logical casesL42–42

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

  1. L42
    cases hb_exists
17Establish hpositiveL43–51

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

  1. L43
    have hpositive : exists p. x = S p
  2. L44
    specialize IH k
  3. L45
    specialize IH x
  4. L46
    apply IH
  5. L47
    specialize le_of_succ_le_succ k
  6. L48
    specialize le_of_succ_le_succ n
  7. L49
    apply le_of_succ_le_succ
  8. L50
    exact hbound
  9. L51
    exact ha_exists_witness
18Separate the logical casesL52–52

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

  1. L52
    cases hpositive
19Establish hsumL53–62

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

  1. L53
    have hsum : z = x + x1
  2. L54
    specialize choose_succ_succ n
  3. L55
    specialize choose_succ_succ k
  4. L56
    specialize choose_succ_succ x
  5. L57
    specialize choose_succ_succ x1
  6. L58
    specialize choose_succ_succ z
  7. L59
    apply choose_succ_succ
  8. L60
    exact ha_exists_witness
  9. L61
    exact hb_exists_witness
  10. L62
    exact hchoose
20Construct an explicit witnessL63–63

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

  1. L63
    exists x2 + x1
21Calculate and transport equalitiesL64–64

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

  1. L64
    trans x + x1
22Use earlier factsL65–65

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

  1. L65
    exact hsum
23Calculate and transport equalitiesL66–66

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

  1. L66
    rewrite hpositive_witness
24Use earlier factsL67–69

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

  1. L67
    specialize add_succ_left x2
  2. L68
    specialize add_succ_left x1
  3. L69
    exact add_succ_left

Library-wide reading audit

Original defined command ledger · 69 lines
  1. 0001induction n
  2. 0002induction k
  3. 0003intro z
  4. 0004intro hbound
  5. 0005intro hchoose
  6. 0006exists 0
  7. 0007specialize choose_zero 0
  8. 0008specialize choose_zero z
  9. 0009apply choose_zero
  10. 0010exact hchoose
  11. 0011intro z
  12. 0012intro hbound
  13. 0013intro hchoose
  14. 0014have hk0 : S k = 0
  15. 0015specialize le_zero (S k)
  16. 0016apply le_zero
  17. 0017exact hbound
  18. 0018exfalso
  19. 0019apply PA1
  20. 0020exact hk0
  21. 0021induction k
  22. 0022intro z
  23. 0023intro hbound
  24. 0024intro hchoose
  25. 0025exists 0
  26. 0026specialize choose_zero (S n)
  27. 0027specialize choose_zero z
  28. 0028apply choose_zero
  29. 0029exact hchoose
  30. 0030intro z
  31. 0031intro hbound
  32. 0032intro hchoose
  33. 0033have ha_exists : ∃ a. Choose(n,k,a)
    Exact native replay linehave ha_exists : exists a. (((exists bcf_lt_gap_bcp_previous_left_out_of_range. bcf_lt_gap_bcp_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcp_previous_left_in_range. bcf_le_gap_bcp_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcp_previous_left bcf_row_code_scale_bcp_previous_left bcf_row_scale_code_bcp_previous_left bcf_row_scale_scale_bcp_previous_left bcf_row_code_bcp_previous_left bcf_row_scale_bcp_previous_left. ((forall bcf_row_index_bcp_previous_left_table. (exists bcf_lt_gap_bcp_previous_left_table_row_bound. bcf_lt_gap_bcp_previous_left_table_row_bound + S (bcf_row_index_bcp_previous_left_table) = S (n)) -> exists bcf_row_code_bcp_previous_left_table bcf_row_scale_bcp_previous_left_table. ((((exists bcf_height_bcp_previous_left_table_decoded_row_code. bcf_height_bcp_previous_left_table_decoded_row_code + S (bcf_row_code_bcp_previous_left_table) = S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_row_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left) + (bcf_row_code_bcp_previous_left_table))) /\ ((((exists bcf_height_bcp_previous_left_table_decoded_row_scale. bcf_height_bcp_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcp_previous_left_table) = S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_row_scale_bcp_previous_left_table))) /\ ((bcf_row_index_bcp_previous_left_table = 0 /\ (forall bcf_index_bcp_previous_left_table_zero_row. (exists bcf_lt_gap_bcp_previous_left_table_zero_row_bound. bcf_lt_gap_bcp_previous_left_table_zero_row_bound + S (bcf_index_bcp_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcp_previous_left_table_zero_row. ((((exists bcf_height_bcp_previous_left_table_zero_row_entry. bcf_height_bcp_previous_left_table_zero_row_entry + S (bcf_value_bcp_previous_left_table_zero_row) = S ((S (bcf_index_bcp_previous_left_table_zero_row)) * bcf_row_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_zero_row_entry. bcf_row_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_zero_row_entry * S ((S (bcf_index_bcp_previous_left_table_zero_row)) * bcf_row_scale_bcp_previous_left_table) + (bcf_value_bcp_previous_left_table_zero_row))) /\ ((bcf_index_bcp_previous_left_table_zero_row = 0 /\ bcf_value_bcp_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcp_previous_left_table_zero_row. bcf_index_bcp_previous_left_table_zero_row = S bcf_predecessor_bcp_previous_left_table_zero_row /\ bcf_value_bcp_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_previous_left_table bcf_previous_code_bcp_previous_left_table bcf_previous_scale_bcp_previous_left_table. bcf_row_index_bcp_previous_left_table = S bcf_predecessor_bcp_previous_left_table /\ ((((exists bcf_height_bcp_previous_left_table_decoded_previous_code. bcf_height_bcp_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcp_previous_left_table) = S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_previous_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_code_scale_bcp_previous_left) + (bcf_previous_code_bcp_previous_left_table))) /\ ((((exists bcf_height_bcp_previous_left_table_decoded_previous_scale. bcf_height_bcp_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcp_previous_left_table) = S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_previous_left_table)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_previous_scale_bcp_previous_left_table))) /\ (forall bcf_index_bcp_previous_left_table_row_step. (exists bcf_lt_gap_bcp_previous_left_table_row_step_bound. bcf_lt_gap_bcp_previous_left_table_row_step_bound + S (bcf_index_bcp_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcp_previous_left_table_row_step. ((((exists bcf_height_bcp_previous_left_table_row_step_entry. bcf_height_bcp_previous_left_table_row_step_entry + S (bcf_value_bcp_previous_left_table_row_step) = S ((S (bcf_index_bcp_previous_left_table_row_step)) * bcf_row_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_entry. bcf_row_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_entry * S ((S (bcf_index_bcp_previous_left_table_row_step)) * bcf_row_scale_bcp_previous_left_table) + (bcf_value_bcp_previous_left_table_row_step))) /\ ((bcf_index_bcp_previous_left_table_row_step = 0 /\ bcf_value_bcp_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcp_previous_left_table_row_step bcf_left_bcp_previous_left_table_row_step bcf_right_bcp_previous_left_table_row_step. bcf_index_bcp_previous_left_table_row_step = S bcf_predecessor_bcp_previous_left_table_row_step /\ ((((exists bcf_height_bcp_previous_left_table_row_step_previous_left. bcf_height_bcp_previous_left_table_row_step_previous_left + S (bcf_left_bcp_previous_left_table_row_step) = S ((S (bcf_predecessor_bcp_previous_left_table_row_step)) * bcf_previous_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_previous_left. bcf_previous_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_previous_left_table_row_step)) * bcf_previous_scale_bcp_previous_left_table) + (bcf_left_bcp_previous_left_table_row_step))) /\ ((((exists bcf_height_bcp_previous_left_table_row_step_previous_right. bcf_height_bcp_previous_left_table_row_step_previous_right + S (bcf_right_bcp_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcp_previous_left_table_row_step))) * bcf_previous_scale_bcp_previous_left_table)) /\ exists bcf_quotient_bcp_previous_left_table_row_step_previous_right. bcf_previous_code_bcp_previous_left_table = bcf_quotient_bcp_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_previous_left_table_row_step))) * bcf_previous_scale_bcp_previous_left_table) + (bcf_right_bcp_previous_left_table_row_step))) /\ bcf_value_bcp_previous_left_table_row_step = bcf_left_bcp_previous_left_table_row_step + bcf_right_bcp_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_previous_left_decoded_row_code. bcf_height_bcp_previous_left_decoded_row_code + S (bcf_row_code_bcp_previous_left) = S ((S (n)) * bcf_row_code_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_row_code. bcf_row_code_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_previous_left) + (bcf_row_code_bcp_previous_left))) /\ ((((exists bcf_height_bcp_previous_left_decoded_row_scale. bcf_height_bcp_previous_left_decoded_row_scale + S (bcf_row_scale_bcp_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_row_scale. bcf_row_scale_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_previous_left) + (bcf_row_scale_bcp_previous_left))) /\ (((exists bcf_height_bcp_previous_left_decoded_value. bcf_height_bcp_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcp_previous_left)) /\ exists bcf_quotient_bcp_previous_left_decoded_value. bcf_row_code_bcp_previous_left = bcf_quotient_bcp_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcp_previous_left) + (a)))))))))
  34. 0034specialize choose_exists n
  35. 0035specialize choose_exists k
  36. 0036exact choose_exists
  37. 0037cases ha_exists
  38. 0038have hb_exists : ∃ b. Choose(n,S k,b)
    Exact native replay linehave hb_exists : exists b. (((exists bcf_lt_gap_bcp_previous_right_out_of_range. bcf_lt_gap_bcp_previous_right_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcp_previous_right_in_range. bcf_le_gap_bcp_previous_right_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcp_previous_right bcf_row_code_scale_bcp_previous_right bcf_row_scale_code_bcp_previous_right bcf_row_scale_scale_bcp_previous_right bcf_row_code_bcp_previous_right bcf_row_scale_bcp_previous_right. ((forall bcf_row_index_bcp_previous_right_table. (exists bcf_lt_gap_bcp_previous_right_table_row_bound. bcf_lt_gap_bcp_previous_right_table_row_bound + S (bcf_row_index_bcp_previous_right_table) = S (n)) -> exists bcf_row_code_bcp_previous_right_table bcf_row_scale_bcp_previous_right_table. ((((exists bcf_height_bcp_previous_right_table_decoded_row_code. bcf_height_bcp_previous_right_table_decoded_row_code + S (bcf_row_code_bcp_previous_right_table) = S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_row_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right) + (bcf_row_code_bcp_previous_right_table))) /\ ((((exists bcf_height_bcp_previous_right_table_decoded_row_scale. bcf_height_bcp_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcp_previous_right_table) = S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_row_scale_bcp_previous_right_table))) /\ ((bcf_row_index_bcp_previous_right_table = 0 /\ (forall bcf_index_bcp_previous_right_table_zero_row. (exists bcf_lt_gap_bcp_previous_right_table_zero_row_bound. bcf_lt_gap_bcp_previous_right_table_zero_row_bound + S (bcf_index_bcp_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcp_previous_right_table_zero_row. ((((exists bcf_height_bcp_previous_right_table_zero_row_entry. bcf_height_bcp_previous_right_table_zero_row_entry + S (bcf_value_bcp_previous_right_table_zero_row) = S ((S (bcf_index_bcp_previous_right_table_zero_row)) * bcf_row_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_zero_row_entry. bcf_row_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_zero_row_entry * S ((S (bcf_index_bcp_previous_right_table_zero_row)) * bcf_row_scale_bcp_previous_right_table) + (bcf_value_bcp_previous_right_table_zero_row))) /\ ((bcf_index_bcp_previous_right_table_zero_row = 0 /\ bcf_value_bcp_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcp_previous_right_table_zero_row. bcf_index_bcp_previous_right_table_zero_row = S bcf_predecessor_bcp_previous_right_table_zero_row /\ bcf_value_bcp_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcp_previous_right_table bcf_previous_code_bcp_previous_right_table bcf_previous_scale_bcp_previous_right_table. bcf_row_index_bcp_previous_right_table = S bcf_predecessor_bcp_previous_right_table /\ ((((exists bcf_height_bcp_previous_right_table_decoded_previous_code. bcf_height_bcp_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcp_previous_right_table) = S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_previous_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_code_scale_bcp_previous_right) + (bcf_previous_code_bcp_previous_right_table))) /\ ((((exists bcf_height_bcp_previous_right_table_decoded_previous_scale. bcf_height_bcp_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcp_previous_right_table) = S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcp_previous_right_table)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_previous_scale_bcp_previous_right_table))) /\ (forall bcf_index_bcp_previous_right_table_row_step. (exists bcf_lt_gap_bcp_previous_right_table_row_step_bound. bcf_lt_gap_bcp_previous_right_table_row_step_bound + S (bcf_index_bcp_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcp_previous_right_table_row_step. ((((exists bcf_height_bcp_previous_right_table_row_step_entry. bcf_height_bcp_previous_right_table_row_step_entry + S (bcf_value_bcp_previous_right_table_row_step) = S ((S (bcf_index_bcp_previous_right_table_row_step)) * bcf_row_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_entry. bcf_row_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_entry * S ((S (bcf_index_bcp_previous_right_table_row_step)) * bcf_row_scale_bcp_previous_right_table) + (bcf_value_bcp_previous_right_table_row_step))) /\ ((bcf_index_bcp_previous_right_table_row_step = 0 /\ bcf_value_bcp_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcp_previous_right_table_row_step bcf_left_bcp_previous_right_table_row_step bcf_right_bcp_previous_right_table_row_step. bcf_index_bcp_previous_right_table_row_step = S bcf_predecessor_bcp_previous_right_table_row_step /\ ((((exists bcf_height_bcp_previous_right_table_row_step_previous_left. bcf_height_bcp_previous_right_table_row_step_previous_left + S (bcf_left_bcp_previous_right_table_row_step) = S ((S (bcf_predecessor_bcp_previous_right_table_row_step)) * bcf_previous_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_previous_left. bcf_previous_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcp_previous_right_table_row_step)) * bcf_previous_scale_bcp_previous_right_table) + (bcf_left_bcp_previous_right_table_row_step))) /\ ((((exists bcf_height_bcp_previous_right_table_row_step_previous_right. bcf_height_bcp_previous_right_table_row_step_previous_right + S (bcf_right_bcp_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcp_previous_right_table_row_step))) * bcf_previous_scale_bcp_previous_right_table)) /\ exists bcf_quotient_bcp_previous_right_table_row_step_previous_right. bcf_previous_code_bcp_previous_right_table = bcf_quotient_bcp_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcp_previous_right_table_row_step))) * bcf_previous_scale_bcp_previous_right_table) + (bcf_right_bcp_previous_right_table_row_step))) /\ bcf_value_bcp_previous_right_table_row_step = bcf_left_bcp_previous_right_table_row_step + bcf_right_bcp_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcp_previous_right_decoded_row_code. bcf_height_bcp_previous_right_decoded_row_code + S (bcf_row_code_bcp_previous_right) = S ((S (n)) * bcf_row_code_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_row_code. bcf_row_code_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcp_previous_right) + (bcf_row_code_bcp_previous_right))) /\ ((((exists bcf_height_bcp_previous_right_decoded_row_scale. bcf_height_bcp_previous_right_decoded_row_scale + S (bcf_row_scale_bcp_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_row_scale. bcf_row_scale_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcp_previous_right) + (bcf_row_scale_bcp_previous_right))) /\ (((exists bcf_height_bcp_previous_right_decoded_value. bcf_height_bcp_previous_right_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcp_previous_right)) /\ exists bcf_quotient_bcp_previous_right_decoded_value. bcf_row_code_bcp_previous_right = bcf_quotient_bcp_previous_right_decoded_value * S ((S (S k)) * bcf_row_scale_bcp_previous_right) + (b)))))))))
  39. 0039specialize choose_exists n
  40. 0040specialize choose_exists (S k)
  41. 0041exact choose_exists
  42. 0042cases hb_exists
  43. 0043have hpositive : exists p. x = S p
  44. 0044specialize IH k
  45. 0045specialize IH x
  46. 0046apply IH
  47. 0047specialize le_of_succ_le_succ k
  48. 0048specialize le_of_succ_le_succ n
  49. 0049apply le_of_succ_le_succ
  50. 0050exact hbound
  51. 0051exact ha_exists_witness
  52. 0052cases hpositive
  53. 0053have hsum : z = x + x1
  54. 0054specialize choose_succ_succ n
  55. 0055specialize choose_succ_succ k
  56. 0056specialize choose_succ_succ x
  57. 0057specialize choose_succ_succ x1
  58. 0058specialize choose_succ_succ z
  59. 0059apply choose_succ_succ
  60. 0060exact ha_exists_witness
  61. 0061exact hb_exists_witness
  62. 0062exact hchoose
  63. 0063exists x2 + x1
  64. 0064trans x + x1
  65. 0065exact hsum
  66. 0066rewrite hpositive_witness
  67. 0067specialize add_succ_left x2
  68. 0068specialize add_succ_left x1
  69. 0069exact add_succ_left