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

At: rem gen base case 1 1

a:, n:. |a| < |n| (a rem n) = a
By:
UnivCD
THEN
BackThru Thm* a:, n:. a < n (a rem n) = a
Generated subgoal:

11. a:
2. n:
3. |a| < |n|
a < n

About:
intremainderless_thanequalimpliesall

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