BT001V

zero_remainder_implies_multiple

Stable · empty-context checked

A quotient decomposition with zero remainder supplies a divisibility witness.

Exact expanded PA statement

forall m n q. n = m * q + 0 -> exists k. n = m * k

Structural proof guide

A quotient decomposition with zero remainder supplies a divisibility witness.

Direct prerequisites: none. The authored body proceeds by equality transport (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT00SH division_successor_quotient_by_bit

Formal native tactic body

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

  1. 0001intro m
  2. 0002intro n
  3. 0003intro q
  4. 0004intro h
  5. 0005exists q
  6. 0006rewrite h
  7. 0007simp