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

At: pos mul arg bounds 1 3 1
1. a:
2. b:
3. ab > 0
4. a > 0

b > 0
By: ReplaceWithEqv (TryC (HigherC IntSimpC)) (ab > a0) 3
Generated subgoal:

13. ab > a0
4. a > 0
b > 0

About:
intnatural_numbermultiply

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