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

At: mul preserves lt 1
1. a:
2. b:
3. n:
4. a < b

na < nb
By: NSubsetInd 3
Generated subgoals:

13. a < b
4. n:
5. 0 < n
6. 1 = n
na < nb
23. a < b
4. n:
5. 1 < n
6. (n-1)a < (n-1)b
na < nb

About:
intmultiplyless_than

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