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

At: rem bounds z 1 1
1. a:
2. b:
3. 0a

|a rem b| < |b|
By:
RWH (LemmaC Thm* i:. |i| = i) 0
THEN
BackThru Thm* a:, n:. 0(a rem n) & (a rem n) < n
Generated subgoals:

None

About:
intnatural_numberremainderless_than

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