Library Coq.Reals.Binomial
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
PartSum
.
Open
Local
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
.