(7steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: rem base case z 1 4
1. a:
2. b:
3. -a < -b
4. 0a
5. 0b

(a rem b) = a
By:
RWH (LemmaC Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)) 0
THEN
Inst Thm* a:, n:. a < n (a rem n) = a [-a;-b]
Generated subgoals:

None

About:
intnatural_numberminusremainderless_thanequal

(7steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc