Step
*
1
of Lemma
subtract_wf
1. x : ℤ
2. y : ℤ
⊢ x - y ∈ ℤ
BY
{ (Unfold `subtract` 0 THEN Auto) }
Latex:
Latex:
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
\mvdash{}  x  -  y  \mmember{}  \mBbbZ{}
By
Latex:
(Unfold  `subtract`  0  THEN  Auto)
Home
Index