(9steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
absval
mul
a,b:
. |a
b| = |a|
|b|
By:
Auto
THEN
CaseNat 0 `a'
Generated subgoals:
1
1.
a:
2.
b:
3.
a = 0
|0
b| = |0|
|b|
1
step
2
1.
a:
2.
b:
3.
a = 0
|a
b| = |a|
|b|
7
steps
About:
(9steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
|0
b| = |0||b|
a = 0 |ab| = |a||b|
a,b:. |ab| = |a||b|
|0b| = |0||b|a = 0 |ab| = |a||b|
