---

Step * of Lemma easy-member-int_seg

No Annotations
∀[i,j,a:ℤ].  (j - a ∈ {i..j-}) supposing (((i + a) ≤ j) and 0 < a)
BY
{ (Auto THEN BLemma `member-int_seg` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[i,j,a:\mBbbZ{}].    (j  -  a  \mmember{}  \{i..j\msupminus{}\})  supposing  (((i  +  a)  \mleq{}  j)  and  0  <  a)


By

---

Latex:
(Auto  THEN  BLemma  `member-int\_seg`  THEN  Auto)

---

Home Index