---

Step * 1 of Lemma gcd_subtract


1. a : ℕ
2. b : ℕ
3. b ≤ a
⊢ gcd(a - b;b) ~ gcd(a;b)
BY
{ TACTIC:((InstLemma `gcd_elim` [⌜a - b⌝;⌜b⌝]⋅ THENA Auto)
          THEN ExRepD
          THEN RWO "-1" 0
          THEN Auto
          THEN (InstLemma `gcd_unique` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
          THEN BHyp -1
          THEN Auto) }

1
1. a : ℕ
2. b : ℕ
3. b ≤ a
4. y : ℤ
5. GCD(a - b;b;y)
6. gcd(a - b;b) = y ∈ ℤ
7. ∀y1,y2:ℤ.  (GCD(a;b;y1) ⇒ GCD(a;b;y2) ⇒ (y1 ~ y2))
⊢ GCD(a;b;y)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  b  \mleq{}  a
\mvdash{}  gcd(a  -  b;b)  \msim{}  gcd(a;b)


By

---

Latex:
TACTIC:((InstLemma  `gcd\_elim`  [\mkleeneopen{}a  -  b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD
                THEN  RWO  "-1"  0
                THEN  Auto
                THEN  (InstLemma  `gcd\_unique`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  BHyp  -1
                THEN  Auto)

---

Home Index