| Some definitions of interest. |
|
reduce_factorization | Def reduce_factorization(f; j)(i) == if i= j f(i)-1 else f(i) fi |
| | Thm* a,b: , f:({a..b }  ), j:{a..b }.
Thm* 0<f(j)  reduce_factorization(f; j) {a..b }   |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |