(5steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
mul
preserves
le
1
2
1.
a:
2.
b:
3.
a
b
4.
n:
5.
0 < n
6.
(n-1)
a
(n-1)
b
n
a
n
b
By:
Assert ((n-1)
a+a
(n-1)
b+b)
Generated subgoal:
1
(n-1)
a+a
(n-1)
b+b
About:
(5steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(n-1)
a+a
(n-1)b+b
ba(n-1)b nanba+a(n-1)b+b) (n-1)a+a(n-1)b+b
