(3steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
multiply
functionality
wrt
le
1
1
1.
i1:
2.
i2:
3.
j1:
4.
j2:
5.
i1
j1
6.
i2
j2
7.
i1
i2
i1
j2
i1
i2
j1
j2
By:
Using [`n',j2] (FwdThru
Thm*
a,b:
, n:
. a
b
n
a
n
b [5])
Generated subgoals:
None
About:
(3steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
j1j2
i2i1j2
i1i2j1j2
a,b:
, n:. ab 
nanb
[5])
