(8steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
seg
ind
1
1
1
1
1.
i:
2.
j:
{i+1...}
3.
E:
{i..j
}
Prop
4.
E(i)
5.
k:{(i+1)..j
}. E(k-1)
E(k)
6.
n:
{i..j
}
7.
k:{i..j
}. k < n
E(k)
E(n)
By:
Decide (n = i)
Generated subgoals:
1
8.
n = i
E(n)
2
8.
n = i
E(n)
About:
(8steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
E(n)
n = i E(n)
}
Prop
k:{(i+1)..j}. E(k-1) 
E(k)}k:{i..j}. k < n E(k) E(n) E(n)n = i E(n)
