---

Step * of Lemma equipollent-int_seg

∀n,m:ℤ.  {n..m-} ~ ℕif n <z m then m - n else 0 fi 
BY
{ (Auto THEN AutoSplit) }

1
1. n : ℤ
2. m : ℤ
3. ¬n < m
⊢ {n..m-} ~ ℕ0

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.    \{n..m\msupminus{}\}  \msim{}  \mBbbN{}if  n  <z  m  then  m  -  n  else  0  fi 


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index