BT00QU

two_mul_eq_add_self

Alpha body-checked · checked-use disabled

Left multiplication by two is explicit doubling.

Exact expanded PA statement

forall n. 2 * n = n + n

Structural proof guide

Left multiplication by two is explicit doubling.

Direct prerequisites: mul_comm, mul_one. The authored body proceeds by equality transport (2).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT000A mul_one

Direct dependents

BT00R4 square_six_shift_identity BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00TU central_binom_succ_recurrence BT00VK central_binom_strong_upper_step BT00VL central_binom_recurrence_double_bundle BT00VP central_binom_odd_middle_le_four_pow BT00VR double_half_predecessor_data BT00VS odd_positive_prefix_predecessor_bound BT00VV primorial_le_four_pow_bounded BT00X4 bertrand_floor_power_product_le_h_from_total BT00X8 bertrand_main_inequality_nat BT0126 bertrand_upper_endpoint_factorization

Formal native tactic body

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

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