BT0046

dvd_to_mod_zero

Stable · empty-context checked

A multiple is balanced-congruent to zero.

Exact expanded PA statement

forall m a. (exists k. a = m * k) -> exists u v. a + m * u = 0 + m * v

Structural proof guide

A multiple is balanced-congruent to zero.

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

Proof neighborhood

Direct dependencies

BT0000 zero_add

Direct dependents

BT004F binary_crt

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 a
  3. 0003intro h
  4. 0004cases h
  5. 0005exists 0
  6. 0006exists x
  7. 0007rewrite h_witness
  8. 0008simp [zero_add]