BT00XF

division_zero_quotient_of_lt

Alpha body-checked · checked-use disabled

A dividend below its divisor has quotient zero.

Exact expanded PA statement

forall d n q r. (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_bdzq_source_bound. bcf_lt_gap_bdzq_source_bound + S (r) = d))) -> (exists bcf_lt_gap_bdzq_bound. bcf_lt_gap_bdzq_bound + S (n) = d) -> q = 0

Structural proof guide

A dividend below its divisor has quotient zero.

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

Proof neighborhood

Direct dependencies

BT0000 zero_add BT001U division_remainder_unique

Direct dependents

BT00XO prime_power_quotient_zero_of_exponent_gt BT00YC double_quotient_carry_prefix_entries_zero

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hdivision
  6. 0006intro hbound
  7. 0007cases hdivision
  8. 0008have hzero : n = d * 0 + n
  9. 0009rewrite PA5
  10. 0010symm
  11. 0011specialize zero_add n
  12. 0012apply zero_add
  13. 0013have hunique : q = 0 /\ r = n
  14. 0014specialize division_remainder_unique d
  15. 0015specialize division_remainder_unique n
  16. 0016specialize division_remainder_unique q
  17. 0017specialize division_remainder_unique r
  18. 0018specialize division_remainder_unique 0
  19. 0019specialize division_remainder_unique n
  20. 0020apply division_remainder_unique
  21. 0021exact hdivision_left
  22. 0022exact hdivision_right
  23. 0023exact hzero
  24. 0024exact hbound
  25. 0025cases hunique
  26. 0026exact hunique_left