PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: rem eq args

a:. (a rem a) = 0
By:
UnivCD
THEN
CondRewriteWith Auto [] [ Thm* a:, n:. an (a rem n) = ((a-n) rem n) ; Thm* a:, n:. a < n (a rem n) = a] 0
Generated subgoals:

None

About:
intnatural_numbersubtractremainderless_thanequalimpliesall

PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc