(6steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: int lower ind 1 1 1 1
1. i:
2. E: {...i}Prop
3. E(i)
4. k:{...i-1}. E(k+1) E(k)
5. j: {...i}
6. k:{...i}. k > j E(k)
7. j = i

E(j)
By:
Assert (j = i)
THEN
RWH (HypC 7) 0
Generated subgoals:

None

About:
intnatural_numberaddsubtractfunctionequalpropimpliesall

(6steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc