(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factorial
tail
split
mid
n
,
m
,
k
:
.
n
k
-
m
m
k
k
!(
n
+
m
) = (
k
-
m
)!
n
k
!
m
By:
Def of <nat>!<nat> THEN ArithSimp Concl
Generated subgoal:
1
1.
n
:
2.
m
:
3.
k
:
4.
n
k
+-
m
5.
m
k
(
i
:{
k
+-
m
+-
n
..
k
}. 1+
i
) = (
i
:{
k
+-
m
+-
n
..
k
+-
m
}. 1+
i
)
(
i
:{
k
+-
m
..
k
}. 1+
i
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
n,m,k:
. n
k-m 
mk k!(n+m) = (k-m)!n
k!m n,m,k:. nk-m mk k!(n+m) = (k-m)!nk!m
k+-m
k
(
i:{k+-m+-n..k
}. 1+i) = ( i:{k+-m+-n..k+-m}. 1+i)( i:{k+-m..k}. 1+i)
