---

Step * of Lemma gcd-positive

∀[y,x:ℕ].  (0 < gcd(x;y)) supposing ((0 ≤ y) and 0 < x)
BY
{ (CompleteInductionOnNat
   THEN Auto
   THEN RecUnfold `gcd` 0
   THEN OldAutoSplit
   THEN (InstLemma `rem_bounds_1` [⌜x⌝;⌜y⌝]⋅ THENA Auto)
   THEN (Decide (x rem y) = 0 ∈ ℤ THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[y,x:\mBbbN{}].    (0  <  gcd(x;y))  supposing  ((0  \mleq{}  y)  and  0  <  x)


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `gcd`  0
  THEN  OldAutoSplit
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Decide  (x  rem  y)  =  0  THENA  Auto))

---

Home Index