Step
*
of Lemma
rem_2_to_1
∀[a:{...0}]. ∀[n:ℕ+]. ((a rem n) = (-(-a rem n)) ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN (RWH (LemmaC `rem_to_div`) 0 THENA Auto)) }
1
1. a : {...0}
2. n : ℕ+
⊢ (a - (a ÷ n) * n) = (-((-a) - ((-a) ÷ n) * n)) ∈ ℤ
Latex:
Latex:
\mforall{}[a:\{...0\}]. \mforall{}[n:\mBbbN{}\msupplus{}]. ((a rem n) = (-(-a rem n)))
By
Latex:
((UnivCD THENA Auto) THEN (RWH (LemmaC `rem\_to\_div`) 0 THENA Auto))
Home
Index