Step
*
of Lemma
rsub-int
∀[n:ℤ]. ∀m:ℤ. ((r(n) - r(m)) = r(n - m))
BY
{ (Auto THEN Unfold `rsub` 0 THEN slowRNorm 0 THEN BLemma `req_weakening` THEN Auto) }
Latex:
Latex:
\mforall{}[n:\mBbbZ{}]. \mforall{}m:\mBbbZ{}. ((r(n) - r(m)) = r(n - m))
By
Latex:
(Auto THEN Unfold `rsub` 0 THEN slowRNorm 0 THEN BLemma `req\_weakening` THEN Auto)
Home
Index