---

Step * 1 of Lemma equipollent-nat-prod-nsub


1. k : ℕ+
2. a1 : ℕ
3. a2 : ℕ
4. <a1 ÷ k, a1 rem k> = <a2 ÷ k, a2 rem k> ∈ (ℕ × ℕk)
⊢ a1 = a2 ∈ ℕ
BY
{ (SplitPair (-1)
   THEN (InstLemma `div_rem_sum` [⌜a1⌝;⌜k⌝]⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜a2⌝;⌜k⌝]⋅ THENA Auto)
   THEN Auto') }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  a1  :  \mBbbN{}
3.  a2  :  \mBbbN{}
4.  <a1  \mdiv{}  k,  a1  rem  k>  =  <a2  \mdiv{}  k,  a2  rem  k>
\mvdash{}  a1  =  a2


By

---

Latex:
(SplitPair  (-1)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto')

---

Home Index