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

At: pos mul arg bounds 2 1

1. a:
2. b:
3. a > 0
4. b > 0

ab > 0

By: BackThru Thm* a,b:. 0 < ab

Generated subgoals:

None


About:
intnatural_numbermultiply

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