BT00Y8

division_quotient_one_of_bounds

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

Bounds between one and two divisors force quotient one.

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.

Exact expanded PA statement

forall d n. (exists bcf_le_gap_bdqob_lower. bcf_le_gap_bdqob_lower + (d) = n) -> (exists bcf_lt_gap_bdqob_upper. bcf_lt_gap_bdqob_upper + S (n) = d + d) -> exists r. (((n) = (d) * (1) + (r) /\ (exists bcf_lt_gap_bdqob_result_bound. bcf_lt_gap_bdqob_result_bound + S (r) = d)))

Structural proof guide

Bounds between one and two divisors force quotient one.

Direct prerequisites: add_comm, mul_one, add_lt_cancel_left. The authored body proceeds by case analysis (1), intermediate claims (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT000A mul_one BT00XC add_lt_cancel_left

Direct dependents

BT00YB division_first_two_of_two_three_range

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

25 script commands · 10 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.

Named ingredients (3)
add commmul oneadd lt cancel left
01Fix variables and assumptionsL1–4

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hlower
  4. L4
    intro hupper
02Separate the logical casesL5–5

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

  1. L5
    cases hlower
03Establish hsumL6–9

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

  1. L6
    have hsum : d + x = n
  2. L7
    trans x + d
  3. L8
    apply add_comm
  4. L9
    exact hlower_witness
04Establish hremainderL10–16

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

  1. L10
    have hremainder : exists bcf_lt_gap_bdqob_remainder. bcf_lt_gap_bdqob_remainder + S (x) = d
  2. L11
    rewrite <- hsum at hupper
  3. L12
    specialize add_lt_cancel_left d
  4. L13
    specialize add_lt_cancel_left x
  5. L14
    specialize add_lt_cancel_left d
  6. L15
    apply add_lt_cancel_left
  7. L16
    exact hupper
05Construct an explicit witnessL17–17

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

  1. L17
    exists x
06Separate the logical casesL18–18

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

  1. L18
    split
07Calculate and transport equalitiesL19–20

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

  1. L19
    trans d + x
  2. L20
    symm
08Use earlier factsL21–22

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

  1. L21
    exact hsum
  2. L22
    specialize mul_one d
09Calculate and transport equalitiesL23–24

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

  1. L23
    rewrite mul_one
  2. L24
    refl
10Use earlier factsL25–25

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

  1. L25
    exact hremainder

Library-wide reading audit

Original exact command ledger · 25 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hlower
  4. 0004intro hupper
  5. 0005cases hlower
  6. 0006have hsum : d + x = n
  7. 0007trans x + d
  8. 0008apply add_comm
  9. 0009exact hlower_witness
  10. 0010have hremainder : exists bcf_lt_gap_bdqob_remainder. bcf_lt_gap_bdqob_remainder + S (x) = d
  11. 0011rewrite <- hsum at hupper
  12. 0012specialize add_lt_cancel_left d
  13. 0013specialize add_lt_cancel_left x
  14. 0014specialize add_lt_cancel_left d
  15. 0015apply add_lt_cancel_left
  16. 0016exact hupper
  17. 0017exists x
  18. 0018split
  19. 0019trans d + x
  20. 0020symm
  21. 0021exact hsum
  22. 0022specialize mul_one d
  23. 0023rewrite mul_one
  24. 0024refl
  25. 0025exact hremainder