Step * of Lemma gcd_sat_gcd_p

a,b:ℤ.  GCD(a;b;gcd(a;b))
BY
(InductionOn ⌜|b|⌝ CompNatInd⋅ THEN Auto THEN RecCaseSplit `gcd` THEN Auto THEN Try ((HypSubst' (-1) 0⋅ THEN Auto))) }

1
.....falsecase..... 
1. : ℕ
2. ∀d:ℕd. ∀a,b:ℤ.  ((|b| ≤ d)  GCD(a;b;gcd(a;b)))
3. : ℤ
4. : ℤ
5. |b| ≤ d
6. ¬(b 0 ∈ ℤ)
⊢ GCD(a;b;gcd(b;a rem b))


Latex:


Latex:
\mforall{}a,b:\mBbbZ{}.    GCD(a;b;gcd(a;b))


By


Latex:
(InductionOn  \mkleeneopen{}|b|\mkleeneclose{}  CompNatInd\mcdot{}
  THEN  Auto
  THEN  RecCaseSplit  `gcd`
  THEN  Auto
  THEN  Try  ((HypSubst'  (-1)  0\mcdot{}  THEN  Auto)))




Home Index