Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n :
m :
z :
n
m
Conclusion:
0
z.1 * m + z.2
Applied Tactic:
D 3
Generated subgoals:
1
. 0
<z1, z2>.1 * m + <z1, z2>.2
n 
m
0 
z.1 * m + z.2 <z1, z2>.1 * m + <z1, z2>.2