Step
*
1
1
1
of Lemma
less-iff-positive
1. x : ℤ
2. y : ℤ
3. x < y
4. 0 < y - x
⊢ 0 < y - x
BY
{ TACTIC:Hypothesis }
Latex:
Latex:
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  x  <  y
4.  0  <  y  -  x
\mvdash{}  0  <  y  -  x
By
Latex:
TACTIC:Hypothesis
Home
Index