---

Step * 2 of Lemma assert_of_lt_int


1. x : ℤ
2. y : ℤ
3. x < y
⊢ ↑x <z y
BY
{ (OnHyp 3 (RepUR_o [Obid: less_than; Obid: less_than']⋅) THEN OnConcl (RepUR_o [Obid: lt_int]⋅)) }

1
1. x : ℤ
2. y : ℤ
3. ↓if (x) < (y)  then True  else False ∧ (x ∈ ℤ) ∧ (y ∈ ℤ)
⊢ ↑if (x) < (y)  then tt  else ff

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  x  <  y
\mvdash{}  \muparrow{}x  <z  y


By

---

Latex:
(OnHyp  3  (RepUR\_o  [Obid:  less\_than;  Obid:  less\_than']\mcdot{})  THEN  OnConcl  (RepUR\_o  [Obid:  lt\_int]\mcdot{}))

---

Home Index