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

At: rem gen base case 1 2 2
1. a:, n:. |a| < |n| (a rem n) = a
2. a:
3. n:
4. |a| < |n|
5. 0a

(a rem n) = a
By: RWH (LemmaC Thm* a:, n:. (a rem n) = -((-a) rem n)) 0
Generated subgoal:

1 -((-a) rem n) = a

About:
intnatural_numberminusremainderless_thanequalimpliesall

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