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