(5steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
mul
preserves
le
1
1.
a:
2.
b:
3.
n:
4.
a
b
n
a
n
b
By:
NInd 3
Generated subgoals:
1
3.
a
b
0
a
0
b
2
3.
a
b
4.
n:
5.
0 < n
6.
(n-1)
a
(n-1)
b
n
a
n
b
About:
(5steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
b
0
a0bb
a(n-1)b nanb
b nanbb 0a0bba(n-1)b nanb
