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

At: rem gen base case


a:, n:. |a| < |n| (a rem n) = a

By: Assert (a:, n:. |a| < |n| (a rem n) = a)

Generated subgoals:

1 a:, n:. |a| < |n| (a rem n) = a
21. a:, n:. |a| < |n| (a rem n) = a
a:, n:. |a| < |n| (a rem n) = a


About:
intremainderless_thanequalimpliesall

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