---

Step * 1 of Lemma assert_of_lt_int


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index