power) == if power=
0
1 else base
(basepower-1) fi (recursive)
Thm* 
n,k:
. (nk) 
Thm* n,k:. (nk)
B == 
B < A
Thm* i,j:. ij Prop
j == if i=j true ; false fi
Thm* i,j:. i=j 
A == A 
False
Thm* A:Prop. (A) Prop
| exp |
Def (basepower) == if power=0 1 else base(basepower-1) fi (recursive)
Thm*
Thm* |
| le |
Def AB == B < A
Thm* |
| eq_int |
Def i=j == if i=j true ; false fi
Thm* |
| not |
Def A == A False
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |