BT002L

is_gcd_zero_right

Stable · empty-context checked

Every natural is the relational gcd of itself and zero.

Exact expanded PA statement

forall a. (((exists x. a = a * x) /\ (exists y. 0 = a * y)) /\ forall c. (exists u. a = c * u) -> (exists v. 0 = c * v) -> exists w. a = c * w)

Structural proof guide

Every natural is the relational gcd of itself and zero.

Direct prerequisites: multiple_refl, multiple_zero. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0028 multiple_refl BT0026 multiple_zero

Direct dependents

BT0034 gcd_balanced_bezout_exists_up_to

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. 0002split
  3. 0003split
  4. 0004specialize multiple_refl a
  5. 0005exact multiple_refl
  6. 0006specialize multiple_zero a
  7. 0007exact multiple_zero
  8. 0008intro c
  9. 0009intro ha
  10. 0010intro hz
  11. 0011exact ha