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

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

-((-a) rem n) = a
By: RWN 2 (IfIsC a (RevLemmaC Thm* a:. -(-a) = a)) 0
Generated subgoal:

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

About:
intnatural_numberminusremainderless_thanequalimpliesall

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