BT00TC · Bertrand theorem

choose_functional

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

The recurrence-defined Choose relation is functional.

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. ∀ x. ∀ y. Choose(n,k,x) → Choose(n,k,y) → x = y

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

PD0041 Choose

2 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall n k x y. (((exists bcf_lt_gap_bclf_left_out_of_range. bcf_lt_gap_bclf_left_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bclf_left_in_range. bcf_le_gap_bclf_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bclf_left bcf_row_code_scale_bclf_left bcf_row_scale_code_bclf_left bcf_row_scale_scale_bclf_left bcf_row_code_bclf_left bcf_row_scale_bclf_left. ((forall bcf_row_index_bclf_left_table. (exists bcf_lt_gap_bclf_left_table_row_bound. bcf_lt_gap_bclf_left_table_row_bound + S (bcf_row_index_bclf_left_table) = S (n)) -> exists bcf_row_code_bclf_left_table bcf_row_scale_bclf_left_table. ((((exists bcf_height_bclf_left_table_decoded_row_code. bcf_height_bclf_left_table_decoded_row_code + S (bcf_row_code_bclf_left_table) = S ((S (bcf_row_index_bclf_left_table)) * bcf_row_code_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_table_decoded_row_code. bcf_row_code_code_bclf_left = bcf_quotient_bclf_left_table_decoded_row_code * S ((S (bcf_row_index_bclf_left_table)) * bcf_row_code_scale_bclf_left) + (bcf_row_code_bclf_left_table))) /\ ((((exists bcf_height_bclf_left_table_decoded_row_scale. bcf_height_bclf_left_table_decoded_row_scale + S (bcf_row_scale_bclf_left_table) = S ((S (bcf_row_index_bclf_left_table)) * bcf_row_scale_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_table_decoded_row_scale. bcf_row_scale_code_bclf_left = bcf_quotient_bclf_left_table_decoded_row_scale * S ((S (bcf_row_index_bclf_left_table)) * bcf_row_scale_scale_bclf_left) + (bcf_row_scale_bclf_left_table))) /\ ((bcf_row_index_bclf_left_table = 0 /\ (forall bcf_index_bclf_left_table_zero_row. (exists bcf_lt_gap_bclf_left_table_zero_row_bound. bcf_lt_gap_bclf_left_table_zero_row_bound + S (bcf_index_bclf_left_table_zero_row) = S (n)) -> exists bcf_value_bclf_left_table_zero_row. ((((exists bcf_height_bclf_left_table_zero_row_entry. bcf_height_bclf_left_table_zero_row_entry + S (bcf_value_bclf_left_table_zero_row) = S ((S (bcf_index_bclf_left_table_zero_row)) * bcf_row_scale_bclf_left_table)) /\ exists bcf_quotient_bclf_left_table_zero_row_entry. bcf_row_code_bclf_left_table = bcf_quotient_bclf_left_table_zero_row_entry * S ((S (bcf_index_bclf_left_table_zero_row)) * bcf_row_scale_bclf_left_table) + (bcf_value_bclf_left_table_zero_row))) /\ ((bcf_index_bclf_left_table_zero_row = 0 /\ bcf_value_bclf_left_table_zero_row = 1) \/ exists bcf_predecessor_bclf_left_table_zero_row. bcf_index_bclf_left_table_zero_row = S bcf_predecessor_bclf_left_table_zero_row /\ bcf_value_bclf_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bclf_left_table bcf_previous_code_bclf_left_table bcf_previous_scale_bclf_left_table. bcf_row_index_bclf_left_table = S bcf_predecessor_bclf_left_table /\ ((((exists bcf_height_bclf_left_table_decoded_previous_code. bcf_height_bclf_left_table_decoded_previous_code + S (bcf_previous_code_bclf_left_table) = S ((S (bcf_predecessor_bclf_left_table)) * bcf_row_code_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_table_decoded_previous_code. bcf_row_code_code_bclf_left = bcf_quotient_bclf_left_table_decoded_previous_code * S ((S (bcf_predecessor_bclf_left_table)) * bcf_row_code_scale_bclf_left) + (bcf_previous_code_bclf_left_table))) /\ ((((exists bcf_height_bclf_left_table_decoded_previous_scale. bcf_height_bclf_left_table_decoded_previous_scale + S (bcf_previous_scale_bclf_left_table) = S ((S (bcf_predecessor_bclf_left_table)) * bcf_row_scale_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_table_decoded_previous_scale. bcf_row_scale_code_bclf_left = bcf_quotient_bclf_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bclf_left_table)) * bcf_row_scale_scale_bclf_left) + (bcf_previous_scale_bclf_left_table))) /\ (forall bcf_index_bclf_left_table_row_step. (exists bcf_lt_gap_bclf_left_table_row_step_bound. bcf_lt_gap_bclf_left_table_row_step_bound + S (bcf_index_bclf_left_table_row_step) = S (n)) -> exists bcf_value_bclf_left_table_row_step. ((((exists bcf_height_bclf_left_table_row_step_entry. bcf_height_bclf_left_table_row_step_entry + S (bcf_value_bclf_left_table_row_step) = S ((S (bcf_index_bclf_left_table_row_step)) * bcf_row_scale_bclf_left_table)) /\ exists bcf_quotient_bclf_left_table_row_step_entry. bcf_row_code_bclf_left_table = bcf_quotient_bclf_left_table_row_step_entry * S ((S (bcf_index_bclf_left_table_row_step)) * bcf_row_scale_bclf_left_table) + (bcf_value_bclf_left_table_row_step))) /\ ((bcf_index_bclf_left_table_row_step = 0 /\ bcf_value_bclf_left_table_row_step = 1) \/ exists bcf_predecessor_bclf_left_table_row_step bcf_left_bclf_left_table_row_step bcf_right_bclf_left_table_row_step. bcf_index_bclf_left_table_row_step = S bcf_predecessor_bclf_left_table_row_step /\ ((((exists bcf_height_bclf_left_table_row_step_previous_left. bcf_height_bclf_left_table_row_step_previous_left + S (bcf_left_bclf_left_table_row_step) = S ((S (bcf_predecessor_bclf_left_table_row_step)) * bcf_previous_scale_bclf_left_table)) /\ exists bcf_quotient_bclf_left_table_row_step_previous_left. bcf_previous_code_bclf_left_table = bcf_quotient_bclf_left_table_row_step_previous_left * S ((S (bcf_predecessor_bclf_left_table_row_step)) * bcf_previous_scale_bclf_left_table) + (bcf_left_bclf_left_table_row_step))) /\ ((((exists bcf_height_bclf_left_table_row_step_previous_right. bcf_height_bclf_left_table_row_step_previous_right + S (bcf_right_bclf_left_table_row_step) = S ((S (S (bcf_predecessor_bclf_left_table_row_step))) * bcf_previous_scale_bclf_left_table)) /\ exists bcf_quotient_bclf_left_table_row_step_previous_right. bcf_previous_code_bclf_left_table = bcf_quotient_bclf_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bclf_left_table_row_step))) * bcf_previous_scale_bclf_left_table) + (bcf_right_bclf_left_table_row_step))) /\ bcf_value_bclf_left_table_row_step = bcf_left_bclf_left_table_row_step + bcf_right_bclf_left_table_row_step))))))))))) /\ ((((exists bcf_height_bclf_left_decoded_row_code. bcf_height_bclf_left_decoded_row_code + S (bcf_row_code_bclf_left) = S ((S (n)) * bcf_row_code_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_decoded_row_code. bcf_row_code_code_bclf_left = bcf_quotient_bclf_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bclf_left) + (bcf_row_code_bclf_left))) /\ ((((exists bcf_height_bclf_left_decoded_row_scale. bcf_height_bclf_left_decoded_row_scale + S (bcf_row_scale_bclf_left) = S ((S (n)) * bcf_row_scale_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_decoded_row_scale. bcf_row_scale_code_bclf_left = bcf_quotient_bclf_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bclf_left) + (bcf_row_scale_bclf_left))) /\ (((exists bcf_height_bclf_left_decoded_value. bcf_height_bclf_left_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bclf_left)) /\ exists bcf_quotient_bclf_left_decoded_value. bcf_row_code_bclf_left = bcf_quotient_bclf_left_decoded_value * S ((S (k)) * bcf_row_scale_bclf_left) + (x))))))))) -> (((exists bcf_lt_gap_bclf_right_out_of_range. bcf_lt_gap_bclf_right_out_of_range + S (n) = k) /\ y = 0) \/ ((exists bcf_le_gap_bclf_right_in_range. bcf_le_gap_bclf_right_in_range + (k) = n) /\ (exists bcf_row_code_code_bclf_right bcf_row_code_scale_bclf_right bcf_row_scale_code_bclf_right bcf_row_scale_scale_bclf_right bcf_row_code_bclf_right bcf_row_scale_bclf_right. ((forall bcf_row_index_bclf_right_table. (exists bcf_lt_gap_bclf_right_table_row_bound. bcf_lt_gap_bclf_right_table_row_bound + S (bcf_row_index_bclf_right_table) = S (n)) -> exists bcf_row_code_bclf_right_table bcf_row_scale_bclf_right_table. ((((exists bcf_height_bclf_right_table_decoded_row_code. bcf_height_bclf_right_table_decoded_row_code + S (bcf_row_code_bclf_right_table) = S ((S (bcf_row_index_bclf_right_table)) * bcf_row_code_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_table_decoded_row_code. bcf_row_code_code_bclf_right = bcf_quotient_bclf_right_table_decoded_row_code * S ((S (bcf_row_index_bclf_right_table)) * bcf_row_code_scale_bclf_right) + (bcf_row_code_bclf_right_table))) /\ ((((exists bcf_height_bclf_right_table_decoded_row_scale. bcf_height_bclf_right_table_decoded_row_scale + S (bcf_row_scale_bclf_right_table) = S ((S (bcf_row_index_bclf_right_table)) * bcf_row_scale_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_table_decoded_row_scale. bcf_row_scale_code_bclf_right = bcf_quotient_bclf_right_table_decoded_row_scale * S ((S (bcf_row_index_bclf_right_table)) * bcf_row_scale_scale_bclf_right) + (bcf_row_scale_bclf_right_table))) /\ ((bcf_row_index_bclf_right_table = 0 /\ (forall bcf_index_bclf_right_table_zero_row. (exists bcf_lt_gap_bclf_right_table_zero_row_bound. bcf_lt_gap_bclf_right_table_zero_row_bound + S (bcf_index_bclf_right_table_zero_row) = S (n)) -> exists bcf_value_bclf_right_table_zero_row. ((((exists bcf_height_bclf_right_table_zero_row_entry. bcf_height_bclf_right_table_zero_row_entry + S (bcf_value_bclf_right_table_zero_row) = S ((S (bcf_index_bclf_right_table_zero_row)) * bcf_row_scale_bclf_right_table)) /\ exists bcf_quotient_bclf_right_table_zero_row_entry. bcf_row_code_bclf_right_table = bcf_quotient_bclf_right_table_zero_row_entry * S ((S (bcf_index_bclf_right_table_zero_row)) * bcf_row_scale_bclf_right_table) + (bcf_value_bclf_right_table_zero_row))) /\ ((bcf_index_bclf_right_table_zero_row = 0 /\ bcf_value_bclf_right_table_zero_row = 1) \/ exists bcf_predecessor_bclf_right_table_zero_row. bcf_index_bclf_right_table_zero_row = S bcf_predecessor_bclf_right_table_zero_row /\ bcf_value_bclf_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bclf_right_table bcf_previous_code_bclf_right_table bcf_previous_scale_bclf_right_table. bcf_row_index_bclf_right_table = S bcf_predecessor_bclf_right_table /\ ((((exists bcf_height_bclf_right_table_decoded_previous_code. bcf_height_bclf_right_table_decoded_previous_code + S (bcf_previous_code_bclf_right_table) = S ((S (bcf_predecessor_bclf_right_table)) * bcf_row_code_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_table_decoded_previous_code. bcf_row_code_code_bclf_right = bcf_quotient_bclf_right_table_decoded_previous_code * S ((S (bcf_predecessor_bclf_right_table)) * bcf_row_code_scale_bclf_right) + (bcf_previous_code_bclf_right_table))) /\ ((((exists bcf_height_bclf_right_table_decoded_previous_scale. bcf_height_bclf_right_table_decoded_previous_scale + S (bcf_previous_scale_bclf_right_table) = S ((S (bcf_predecessor_bclf_right_table)) * bcf_row_scale_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_table_decoded_previous_scale. bcf_row_scale_code_bclf_right = bcf_quotient_bclf_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bclf_right_table)) * bcf_row_scale_scale_bclf_right) + (bcf_previous_scale_bclf_right_table))) /\ (forall bcf_index_bclf_right_table_row_step. (exists bcf_lt_gap_bclf_right_table_row_step_bound. bcf_lt_gap_bclf_right_table_row_step_bound + S (bcf_index_bclf_right_table_row_step) = S (n)) -> exists bcf_value_bclf_right_table_row_step. ((((exists bcf_height_bclf_right_table_row_step_entry. bcf_height_bclf_right_table_row_step_entry + S (bcf_value_bclf_right_table_row_step) = S ((S (bcf_index_bclf_right_table_row_step)) * bcf_row_scale_bclf_right_table)) /\ exists bcf_quotient_bclf_right_table_row_step_entry. bcf_row_code_bclf_right_table = bcf_quotient_bclf_right_table_row_step_entry * S ((S (bcf_index_bclf_right_table_row_step)) * bcf_row_scale_bclf_right_table) + (bcf_value_bclf_right_table_row_step))) /\ ((bcf_index_bclf_right_table_row_step = 0 /\ bcf_value_bclf_right_table_row_step = 1) \/ exists bcf_predecessor_bclf_right_table_row_step bcf_left_bclf_right_table_row_step bcf_right_bclf_right_table_row_step. bcf_index_bclf_right_table_row_step = S bcf_predecessor_bclf_right_table_row_step /\ ((((exists bcf_height_bclf_right_table_row_step_previous_left. bcf_height_bclf_right_table_row_step_previous_left + S (bcf_left_bclf_right_table_row_step) = S ((S (bcf_predecessor_bclf_right_table_row_step)) * bcf_previous_scale_bclf_right_table)) /\ exists bcf_quotient_bclf_right_table_row_step_previous_left. bcf_previous_code_bclf_right_table = bcf_quotient_bclf_right_table_row_step_previous_left * S ((S (bcf_predecessor_bclf_right_table_row_step)) * bcf_previous_scale_bclf_right_table) + (bcf_left_bclf_right_table_row_step))) /\ ((((exists bcf_height_bclf_right_table_row_step_previous_right. bcf_height_bclf_right_table_row_step_previous_right + S (bcf_right_bclf_right_table_row_step) = S ((S (S (bcf_predecessor_bclf_right_table_row_step))) * bcf_previous_scale_bclf_right_table)) /\ exists bcf_quotient_bclf_right_table_row_step_previous_right. bcf_previous_code_bclf_right_table = bcf_quotient_bclf_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bclf_right_table_row_step))) * bcf_previous_scale_bclf_right_table) + (bcf_right_bclf_right_table_row_step))) /\ bcf_value_bclf_right_table_row_step = bcf_left_bclf_right_table_row_step + bcf_right_bclf_right_table_row_step))))))))))) /\ ((((exists bcf_height_bclf_right_decoded_row_code. bcf_height_bclf_right_decoded_row_code + S (bcf_row_code_bclf_right) = S ((S (n)) * bcf_row_code_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_decoded_row_code. bcf_row_code_code_bclf_right = bcf_quotient_bclf_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bclf_right) + (bcf_row_code_bclf_right))) /\ ((((exists bcf_height_bclf_right_decoded_row_scale. bcf_height_bclf_right_decoded_row_scale + S (bcf_row_scale_bclf_right) = S ((S (n)) * bcf_row_scale_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_decoded_row_scale. bcf_row_scale_code_bclf_right = bcf_quotient_bclf_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bclf_right) + (bcf_row_scale_bclf_right))) /\ (((exists bcf_height_bclf_right_decoded_value. bcf_height_bclf_right_decoded_value + S (y) = S ((S (k)) * bcf_row_scale_bclf_right)) /\ exists bcf_quotient_bclf_right_decoded_value. bcf_row_code_bclf_right = bcf_quotient_bclf_right_decoded_value * S ((S (k)) * bcf_row_scale_bclf_right) + (y))))))))) -> x = y

Proof neighborhood

Direct theorem prerequisites

BT001I lt_not_le BT000E le_refl BT0016 succ_le_succ BT00TB beta_pascal_table_row_pointwise_functional

Direct theorem dependents

BT00VL central_binom_recurrence_double_bundle

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

92 script commands · 18 reading checkpoints · 3 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 (4)
lt not lele reflsucc le succbeta pascal table row pointwise functional
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hleft
  6. L6
    intro hright
02Separate the logical casesL7–10

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

  1. L7
    cases hleft
  2. L8
    cases hleft_left
  3. L9
    cases hright
  4. L10
    cases hright_left
03Calculate and transport equalitiesL11–11

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

  1. L11
    trans 0
04Use earlier factsL12–12

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

  1. L12
    exact hleft_left_right
05Calculate and transport equalitiesL13–13

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

  1. L13
    symm
06Use earlier factsL14–14

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

  1. L14
    exact hright_left_right
07Separate the logical casesL15–16

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

  1. L15
    cases hright_right
  2. L16
    exfalso
08Use earlier factsL17–21

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

  1. L17
    specialize lt_not_le n
  2. L18
    specialize lt_not_le k
  3. L19
    apply lt_not_le
  4. L20
    exact hleft_left_left
  5. L21
    exact hright_right_left
09Separate the logical casesL22–25

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

  1. L22
    cases hleft_right
  2. L23
    cases hright
  3. L24
    cases hright_left
  4. L25
    exfalso
10Use earlier factsL26–30

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

  1. L26
    specialize lt_not_le n
  2. L27
    specialize lt_not_le k
  3. L28
    apply lt_not_le
  4. L29
    exact hright_left_left
  5. L30
    exact hleft_right_left
11Separate the logical casesL31–40

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

  1. L31
    cases hright_right
  2. L32
    cases hleft_right_right
  3. L33
    cases hleft_right_right_witness
  4. L34
    cases hleft_right_right_witness_witness
  5. L35
    cases hleft_right_right_witness_witness_witness
  6. L36
    cases hleft_right_right_witness_witness_witness_witness
  7. L37
    cases hleft_right_right_witness_witness_witness_witness_witness
  8. L38
    cases hleft_right_right_witness_witness_witness_witness_witness_witness
  9. L39
    cases hleft_right_right_witness_witness_witness_witness_witness_witness_right
  10. L40
    cases hleft_right_right_witness_witness_witness_witness_witness_witness_right_right
12Separate the logical casesL41–49

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

  1. L41
    cases hright_right_right
  2. L42
    cases hright_right_right_witness
  3. L43
    cases hright_right_right_witness_witness
  4. L44
    cases hright_right_right_witness_witness_witness
  5. L45
    cases hright_right_right_witness_witness_witness_witness
  6. L46
    cases hright_right_right_witness_witness_witness_witness_witness
  7. L47
    cases hright_right_right_witness_witness_witness_witness_witness_witness
  8. L48
    cases hright_right_right_witness_witness_witness_witness_witness_witness_right
  9. L49
    cases hright_right_right_witness_witness_witness_witness_witness_witness_right_right
13Establish hrow_boundL50–52

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

  1. L50
    have hrow_bound : Lt(n,S n)Definitions: Lt(n,S n)Original native command in the exact edition
  2. L51
    specialize le_refl (S n)
  3. L52
    exact le_refl
14Establish hinner_boundL53–57

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

  1. L53
    have hinner_bound : Lt(k,S n)Definitions: Lt(k,S n)Original native command in the exact edition
  2. L54
    specialize succ_le_succ k
  3. L55
    specialize succ_le_succ n
  4. L56
    apply succ_le_succ
  5. L57
    exact hleft_right_left
15Establish hagreeL58–67

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

  1. L58
    have hagree : ∀ bcf_index_bclf_semantic_agreement. ∀ bcf_left_value_bclf_semantic_agreement. ∀ bcf_right_value_bclf_semantic_agreement. Lt(bcf_index_bclf_semantic_agreement,S n) → Lt(bcf_index_bclf_semantic_agreement,S n) → BetaAt(x5,x6,bcf_index_bclf_semantic_agreement,bcf_left_value_bclf_semantic_agreement) → BetaAt(x11,x12,bcf_index_bclf_semantic_agreement,bcf_right_value_bclf_semantic_agreement) → bcf_left_value_bclf_semantic_agreement = bcf_right_value_bclf_semantic_agreementDefinitions: Lt(bcf_index_bclf_semantic_agreement,S n)BetaAt(x5,x6,bcf_index_bclf_semantic_agreement,bcf_left_value_bclf_semantic_agreement)BetaAt(x11,x12,bcf_index_bclf_semantic_agreement,bcf_right_value_bclf_semantic_agreement)Original native command in the exact edition
  2. L59
    specialize beta_pascal_table_row_pointwise_functional x1
  3. L60
    specialize beta_pascal_table_row_pointwise_functional x2
  4. L61
    specialize beta_pascal_table_row_pointwise_functional x3
  5. L62
    specialize beta_pascal_table_row_pointwise_functional x4
  6. L63
    specialize beta_pascal_table_row_pointwise_functional (S n)
  7. L64
    specialize beta_pascal_table_row_pointwise_functional (S n)
  8. L65
    specialize beta_pascal_table_row_pointwise_functional x7
  9. L66
    specialize beta_pascal_table_row_pointwise_functional x8
  10. L67
    specialize beta_pascal_table_row_pointwise_functional x9
16Use earlier factsL68–77

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

  1. L68
    specialize beta_pascal_table_row_pointwise_functional x10
  2. L69
    specialize beta_pascal_table_row_pointwise_functional (S n)
  3. L70
    specialize beta_pascal_table_row_pointwise_functional (S n)
  4. L71
    specialize beta_pascal_table_row_pointwise_functional n
  5. L72
    specialize beta_pascal_table_row_pointwise_functional x5
  6. L73
    specialize beta_pascal_table_row_pointwise_functional x6
  7. L74
    specialize beta_pascal_table_row_pointwise_functional x11
  8. L75
    specialize beta_pascal_table_row_pointwise_functional x12
  9. L76
    apply beta_pascal_table_row_pointwise_functional
  10. L77
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_left
17Use earlier factsL78–87

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

  1. L78
    exact hright_right_right_witness_witness_witness_witness_witness_witness_left
  2. L79
    exact hrow_bound
  3. L80
    exact hrow_bound
  4. L81
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_left
  5. L82
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  6. L83
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_left
  7. L84
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  8. L85
    specialize hagree k
  9. L86
    specialize hagree x
  10. L87
    specialize hagree y
18Use earlier factsL88–92

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

  1. L88
    apply hagree
  2. L89
    exact hinner_bound
  3. L90
    exact hinner_bound
  4. L91
    exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  5. L92
    exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hleft
  6. 0006intro hright
  7. 0007cases hleft
  8. 0008cases hleft_left
  9. 0009cases hright
  10. 0010cases hright_left
  11. 0011trans 0
  12. 0012exact hleft_left_right
  13. 0013symm
  14. 0014exact hright_left_right
  15. 0015cases hright_right
  16. 0016exfalso
  17. 0017specialize lt_not_le n
  18. 0018specialize lt_not_le k
  19. 0019apply lt_not_le
  20. 0020exact hleft_left_left
  21. 0021exact hright_right_left
  22. 0022cases hleft_right
  23. 0023cases hright
  24. 0024cases hright_left
  25. 0025exfalso
  26. 0026specialize lt_not_le n
  27. 0027specialize lt_not_le k
  28. 0028apply lt_not_le
  29. 0029exact hright_left_left
  30. 0030exact hleft_right_left
  31. 0031cases hright_right
  32. 0032cases hleft_right_right
  33. 0033cases hleft_right_right_witness
  34. 0034cases hleft_right_right_witness_witness
  35. 0035cases hleft_right_right_witness_witness_witness
  36. 0036cases hleft_right_right_witness_witness_witness_witness
  37. 0037cases hleft_right_right_witness_witness_witness_witness_witness
  38. 0038cases hleft_right_right_witness_witness_witness_witness_witness_witness
  39. 0039cases hleft_right_right_witness_witness_witness_witness_witness_witness_right
  40. 0040cases hleft_right_right_witness_witness_witness_witness_witness_witness_right_right
  41. 0041cases hright_right_right
  42. 0042cases hright_right_right_witness
  43. 0043cases hright_right_right_witness_witness
  44. 0044cases hright_right_right_witness_witness_witness
  45. 0045cases hright_right_right_witness_witness_witness_witness
  46. 0046cases hright_right_right_witness_witness_witness_witness_witness
  47. 0047cases hright_right_right_witness_witness_witness_witness_witness_witness
  48. 0048cases hright_right_right_witness_witness_witness_witness_witness_witness_right
  49. 0049cases hright_right_right_witness_witness_witness_witness_witness_witness_right_right
  50. 0050have hrow_bound : Lt(n,S n)
    Exact native replay linehave hrow_bound : exists bcf_lt_gap_bclf_row_bound. bcf_lt_gap_bclf_row_bound + S (n) = S n
  51. 0051specialize le_refl (S n)
  52. 0052exact le_refl
  53. 0053have hinner_bound : Lt(k,S n)
    Exact native replay linehave hinner_bound : exists bcf_lt_gap_bclf_inner_bound. bcf_lt_gap_bclf_inner_bound + S (k) = S n
  54. 0054specialize succ_le_succ k
  55. 0055specialize succ_le_succ n
  56. 0056apply succ_le_succ
  57. 0057exact hleft_right_left
  58. 0058have hagree : ∀ bcf_index_bclf_semantic_agreement. ∀ bcf_left_value_bclf_semantic_agreement. ∀ bcf_right_value_bclf_semantic_agreement. Lt(bcf_index_bclf_semantic_agreement,S n) → Lt(bcf_index_bclf_semantic_agreement,S n) → BetaAt(x5,x6,bcf_index_bclf_semantic_agreement,bcf_left_value_bclf_semantic_agreement) → BetaAt(x11,x12,bcf_index_bclf_semantic_agreement,bcf_right_value_bclf_semantic_agreement) → bcf_left_value_bclf_semantic_agreement = bcf_right_value_bclf_semantic_agreement
    Exact native replay linehave hagree : forall bcf_index_bclf_semantic_agreement bcf_left_value_bclf_semantic_agreement bcf_right_value_bclf_semantic_agreement. (exists bcf_lt_gap_bclf_semantic_agreement_left_bound. bcf_lt_gap_bclf_semantic_agreement_left_bound + S (bcf_index_bclf_semantic_agreement) = S n) -> (exists bcf_lt_gap_bclf_semantic_agreement_right_bound. bcf_lt_gap_bclf_semantic_agreement_right_bound + S (bcf_index_bclf_semantic_agreement) = S n) -> (((exists bcf_height_bclf_semantic_agreement_left_entry. bcf_height_bclf_semantic_agreement_left_entry + S (bcf_left_value_bclf_semantic_agreement) = S ((S (bcf_index_bclf_semantic_agreement)) * x6)) /\ exists bcf_quotient_bclf_semantic_agreement_left_entry. x5 = bcf_quotient_bclf_semantic_agreement_left_entry * S ((S (bcf_index_bclf_semantic_agreement)) * x6) + (bcf_left_value_bclf_semantic_agreement))) -> (((exists bcf_height_bclf_semantic_agreement_right_entry. bcf_height_bclf_semantic_agreement_right_entry + S (bcf_right_value_bclf_semantic_agreement) = S ((S (bcf_index_bclf_semantic_agreement)) * x12)) /\ exists bcf_quotient_bclf_semantic_agreement_right_entry. x11 = bcf_quotient_bclf_semantic_agreement_right_entry * S ((S (bcf_index_bclf_semantic_agreement)) * x12) + (bcf_right_value_bclf_semantic_agreement))) -> bcf_left_value_bclf_semantic_agreement = bcf_right_value_bclf_semantic_agreement
  59. 0059specialize beta_pascal_table_row_pointwise_functional x1
  60. 0060specialize beta_pascal_table_row_pointwise_functional x2
  61. 0061specialize beta_pascal_table_row_pointwise_functional x3
  62. 0062specialize beta_pascal_table_row_pointwise_functional x4
  63. 0063specialize beta_pascal_table_row_pointwise_functional (S n)
  64. 0064specialize beta_pascal_table_row_pointwise_functional (S n)
  65. 0065specialize beta_pascal_table_row_pointwise_functional x7
  66. 0066specialize beta_pascal_table_row_pointwise_functional x8
  67. 0067specialize beta_pascal_table_row_pointwise_functional x9
  68. 0068specialize beta_pascal_table_row_pointwise_functional x10
  69. 0069specialize beta_pascal_table_row_pointwise_functional (S n)
  70. 0070specialize beta_pascal_table_row_pointwise_functional (S n)
  71. 0071specialize beta_pascal_table_row_pointwise_functional n
  72. 0072specialize beta_pascal_table_row_pointwise_functional x5
  73. 0073specialize beta_pascal_table_row_pointwise_functional x6
  74. 0074specialize beta_pascal_table_row_pointwise_functional x11
  75. 0075specialize beta_pascal_table_row_pointwise_functional x12
  76. 0076apply beta_pascal_table_row_pointwise_functional
  77. 0077exact hleft_right_right_witness_witness_witness_witness_witness_witness_left
  78. 0078exact hright_right_right_witness_witness_witness_witness_witness_witness_left
  79. 0079exact hrow_bound
  80. 0080exact hrow_bound
  81. 0081exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_left
  82. 0082exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  83. 0083exact hright_right_right_witness_witness_witness_witness_witness_witness_right_left
  84. 0084exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  85. 0085specialize hagree k
  86. 0086specialize hagree x
  87. 0087specialize hagree y
  88. 0088apply hagree
  89. 0089exact hinner_bound
  90. 0090exact hinner_bound
  91. 0091exact hleft_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  92. 0092exact hright_right_right_witness_witness_witness_witness_witness_witness_right_right_right