At: prod fin is fin 1 2 6 2 1 1 1 4 3
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. a: n
11. f(a) = b1
12. a1: n
13. f(a1) = b2
14. a2: (n
n)
0
(a2 rem n)
By:
Inst
Thm* a:, n:
. 0(a rem n) & (a rem n) < n
[a2;n]
THEN
ProveProp
Generated subgoals:None
About:
