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

At: rem eq args z


a:, b:. |a| = |b| (a rem b) = 0

By:
Assert (a:, b:. |a| = b (a rem b) = 0)
THEN
UnivCD


Generated subgoals:

11. a:
2. b:
3. |a| = b
(a rem b) = 0
21. a:, b:. |a| = b (a rem b) = 0
2. a:
3. b:
4. |a| = |b|
(a rem b) = 0


About:
intnatural_numberremainderequalimpliesall

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