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

At: mul preserves lt 1 2 1
1. a:
2. b:
3. a+1b
4. n:
5. 1 < n
6. (n-1)a+1(n-1)b

na < nb
By: FwdThru Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 [3;6]
Generated subgoal:

17. a+1+(n-1)a+1b+(n-1)b
na < nb

About:
intnatural_numberaddsubtractmultiplyless_than

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