---

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

.....subterm..... T:t
1:n
1. k : ℕ+
2. b1 : ℕ
3. b2 : ℕk
⊢ (((k * b1) + b2) ÷ k) = b1 ∈ ℕ
BY
{ xxx((Symmetry THEN EqTypeCD) THEN Auto THEN Symmetry)xxx }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  k  :  \mBbbN{}\msupplus{}
2.  b1  :  \mBbbN{}
3.  b2  :  \mBbbN{}k
\mvdash{}  (((k  *  b1)  +  b2)  \mdiv{}  k)  =  b1


By

---

Latex:
xxx((Symmetry  THEN  EqTypeCD)  THEN  Auto  THEN  Symmetry)xxx

---

Home Index