(9steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: absval mul 2 1

1. a:
2. b:
3. a = 0
4. b = 0
|a0| = |a||0|

By:
Subst (a0 = 0) 0
THEN
Subst (|0| = 0) 0
THEN
Unfold `absval` 0
THEN
Reduce 0


Generated subgoals:

None

About:
intnatural_numbermultiplyequal

(9steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc