---

Step * of Lemma equipollent-nat-prod-nsub

∀k:ℕ+. ℕ ~ ℕ × ℕk
BY
{ xxx(Auto
      THEN With ⌜λn.<n ÷ k, n rem k>⌝ (D 0)⋅
      THEN Auto
      THEN Try ((InstLemma `rem_bounds_1` [⌜n⌝;⌜k⌝]⋅ THEN Auto))
      THEN RepeatFor 2 (D 0⋅)
      THEN Reduce 0
      THEN Auto
      THEN Try ((BLemma `rem_bounds_1` ⋅ THEN Auto)))xxx }

1
1. k : ℕ+
2. a1 : ℕ
3. a2 : ℕ
4. <a1 ÷ k, a1 rem k> = <a2 ÷ k, a2 rem k> ∈ (ℕ × ℕk)
⊢ a1 = a2 ∈ ℕ

2
1. k : ℕ+
2. b : ℕ × ℕk
⊢ ∃a:ℕ. (<a ÷ k, a rem k> = b ∈ (ℕ × ℕk))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}\msupplus{}.  \mBbbN{}  \msim{}  \mBbbN{}  \mtimes{}  \mBbbN{}k


By

---

Latex:
xxx(Auto
        THEN  With  \mkleeneopen{}\mlambda{}n.<n  \mdiv{}  k,  n  rem  k>\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  Try  ((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto))
        THEN  RepeatFor  2  (D  0\mcdot{})
        THEN  Reduce  0
        THEN  Auto
        THEN  Try  ((BLemma  `rem\_bounds\_1`  \mcdot{}  THEN  Auto)))xxx

---

Home Index