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