Library Coq.Reals.Binomial
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
PartSum
.
Local
Open
Scope
R_scope
.
Definition
C
(
n
p
:
nat
) :
R
:=
INR
(
fact
n
)
/
(
INR
(
fact
p
)
*
INR
(
fact
(
n
-
p
))
)
.
Lemma
pascal_step1
:
forall
n
i
:
nat
, (
i
<=
n
)%
nat
->
C
n
i
=
C
n
(
n
-
i
).
Lemma
pascal_step2
:
forall
n
i
:
nat
,
(
i
<=
n
)%
nat
->
C
(
S
n
)
i
=
INR
(
S
n
)
/
INR
(
S
n
-
i
)
*
C
n
i
.
Lemma
pascal_step3
:
forall
n
i
:
nat
, (
i
<
n
)%
nat
->
C
n
(
S
i
)
=
INR
(
n
-
i
)
/
INR
(
S
i
)
*
C
n
i
.
Lemma
pascal
:
forall
n
i
:
nat
, (
i
<
n
)%
nat
->
C
n
i
+
C
n
(
S
i
)
=
C
(
S
n
) (
S
i
).
Lemma
binomial
:
forall
(
x
y
:
R
) (
n
:
nat
),
(
x
+
y
)
^
n
=
sum_f_R0
(
fun
i
:
nat
=>
C
n
i
*
x
^
i
*
y
^
(
n
-
i
)
)
n
.