Step * 1 1 1 1 2 2 of Lemma absval_cases

.....wf..... 
1. : ℤ
2. : ℕ
3. 0 < x
⊢ y ∈ ℤ ∈ ℙ
BY
Auto }


Latex:


Latex:
.....wf..... 
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbN{}
3.  0  <  x
\mvdash{}  x  =  y  \mmember{}  \mBbbP{}


By


Latex:
Auto




Home Index