---

Step * of Lemma nat-to-incomparable-property

∀[n,m:ℕ].  ¬nat-to-incomparable(n) ≤ nat-to-incomparable(m) supposing ¬(n = m ∈ ℤ)
BY
{ ((Auto THEN Try (Fold `name` 0 THEN Auto⋅))
   THEN (D 0 THENA Auto)
   THEN Try (Fold `name` 0 THEN Auto⋅)
   THEN (Unfold `nat-to-incomparable` -1 THEN (RWO "iseg_append_iff" (-1) THENM D -1) THEN Auto)) }

1
1. n : ℕ
2. m : ℕ
3. ¬(n = m ∈ ℤ)
4. nat-to-str(n) @ [/] ≤ nat-to-str(m)
⊢ False

2
1. n : ℕ
2. m : ℕ
3. ¬(n = m ∈ ℤ)
4. ∃l:Atom List. (0 < ||l|| ∧ ((nat-to-str(n) @ [/]) = (nat-to-str(m) @ l) ∈ (Atom List)) ∧ l ≤ [/])
⊢ False

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    \mneg{}nat-to-incomparable(n)  \mleq{}  nat-to-incomparable(m)  supposing  \mneg{}(n  =  m)


By

---

Latex:
((Auto  THEN  Try  (Fold  `name`  0  THEN  Auto\mcdot{}))
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Fold  `name`  0  THEN  Auto\mcdot{})
  THEN  (Unfold  `nat-to-incomparable`  -1  THEN  (RWO  "iseg\_append\_iff"  (-1)  THENM  D  -1)  THEN  Auto))

---

Home Index