---

Step * 2 of Lemma equipollent-add


1. a : ℕ@i
2. b : ℕ@i
3. b@0 : ℕa + b@i
⊢ ∃a@0:ℕa + ℕb. (case a@0 of inl(x) => x | inr(y) => a + y = b@0 ∈ ℕa + b)
BY
{ (Decide b@0 < a THENA Auto) }

1
1. a : ℕ@i
2. b : ℕ@i
3. b@0 : ℕa + b@i
4. b@0 < a
⊢ ∃a@0:ℕa + ℕb. (case a@0 of inl(x) => x | inr(y) => a + y = b@0 ∈ ℕa + b)

2
1. a : ℕ@i
2. b : ℕ@i
3. b@0 : ℕa + b@i
4. ¬b@0 < a
⊢ ∃a@0:ℕa + ℕb. (case a@0 of inl(x) => x | inr(y) => a + y = b@0 ∈ ℕa + b)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}@i
2.  b  :  \mBbbN{}@i
3.  b@0  :  \mBbbN{}a  +  b@i
\mvdash{}  \mexists{}a@0:\mBbbN{}a  +  \mBbbN{}b.  (case  a@0  of  inl(x)  =>  x  |  inr(y)  =>  a  +  y  =  b@0)


By

---

Latex:
(Decide  b@0  <  a  THENA  Auto)

---

Home Index