At: prod fin is fin 1 2 6 2 1 1 1 3 1 1 1 2 1
1. T: Type
2. t: T
3. n: 
4. f: n
T
5. Inj(n; T; f)
6. 
b:T. 
a:n. f(a) = b
7. n > 0
8. b1: T
9. b2: T
10. a1: n
11. f(a1) = b2
12. a: 
13. 0 < a
14. 0
a
15. a < n
16. a-1 = (((a-1)
n+a1) 
n)
0an+a1
By: Inst
Thm* a,b:. 0ab
[a;n]
Generated subgoals:None
About:
