---

Step * 1 of Lemma gcd-mod


1. x : ℕ+
2. y : ℕ
3. y = 0 ∈ ℤ
⊢ gcd(x;0 mod x) = gcd(x;0) ∈ ℤ
BY
{ ((EqCD THEN Auto) THEN Unfold `modulus` 0 THEN Reduce 0 THEN RWO "zero-rem" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}
2.  y  :  \mBbbN{}
3.  y  =  0
\mvdash{}  gcd(x;0  mod  x)  =  gcd(x;0)


By

---

Latex:
((EqCD  THEN  Auto)  THEN  Unfold  `modulus`  0  THEN  Reduce  0  THEN  RWO  "zero-rem"  0  THEN  Auto)

---

Home Index