Step * 1 2 1 1 of Lemma polynom-equal-iff


1. n : ℤ
2. p : ℤ
3. q : ℤ
4. ↑(p + (-q) =z 0)
⊢ p = q ∈ ℤ
BY
{ (RW assert_pushdownC (-1) THEN Auto) }


Latex:


Latex:

1.  n  :  \mBbbZ{}
2.  p  :  \mBbbZ{}
3.  q  :  \mBbbZ{}
4.  \muparrow{}(p  +  (-q)  =\msubz{}  0)
\mvdash{}  p  =  q


By


Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)




Home Index