---

Step * 2 1 of Lemma equipollent-nsub


1. n : ℕ
2. m : ℕ
3. ℕn ~ ℕm
4. ℕm ~ ℕn
⊢ n = m ∈ ℤ
BY
{ xxx((Assert n ≤ m BY
             (RepeatFor 2 (D -2) THEN FLemma `pigeon-hole` [-3] THEN Auto))
      THEN (Assert m ≤ n BY
                  (RepeatFor 2 (D -2) THEN FLemma `pigeon-hole` [-3] THEN Auto))
      )xxx }

1
1. n : ℕ
2. m : ℕ
3. ℕn ~ ℕm
4. ℕm ~ ℕn
5. n ≤ m
6. m ≤ n
⊢ n = m ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mBbbN{}n  \msim{}  \mBbbN{}m
4.  \mBbbN{}m  \msim{}  \mBbbN{}n
\mvdash{}  n  =  m


By

---

Latex:
xxx((Assert  n  \mleq{}  m  BY
                      (RepeatFor  2  (D  -2)  THEN  FLemma  `pigeon-hole`  [-3]  THEN  Auto))
        THEN  (Assert  m  \mleq{}  n  BY
                                (RepeatFor  2  (D  -2)  THEN  FLemma  `pigeon-hole`  [-3]  THEN  Auto))
        )xxx

---

Home Index