BT00RE

three_mul_eq_two_mul_add_self

Alpha body-checked · checked-use disabled

Left multiplication by three is twice the input plus the input.

Exact expanded PA statement

forall a. 3 * a = 2 * a + a

Structural proof guide

Left multiplication by three is twice the input plus the input.

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

Proof neighborhood

Direct dependencies

BT0006 mul_comm

Direct dependents

BT00RG double_triple_remainder_complement_budget

Formal native tactic body

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

  1. 0001intro a
  2. 0002trans a * 3
  3. 0003apply mul_comm
  4. 0004rewrite PA6
  5. 0005congr
  6. 0006apply mul_comm
  7. 0007refl