diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 7 |
2 files changed, 9 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ba58cb3..5964257 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,7 +18,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added theorem `totient_prime` in `prime.v` -- Added theorems `prime_modn_expSn` and `fermat_little` in `binomial.v` +- Added theorems `ffact_prod`,`prime_modn_expSn` and `fermat_little` + in `binomial.v` ### Changed diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 5896858..0c5be52 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -148,6 +148,13 @@ elim: n m => [|n IHn] [|m] //=; first by rewrite ffactn1 mul1n. by rewrite !ffactSS IHn mulnA. Qed. +Lemma ffact_prod n m : n ^_ m = \prod_(i < m) (n - i). +Proof. +elim: m n => [n | m IH [|n] //]; first by rewrite ffactn0 big_ord0. + by rewrite big_ord_recr /= sub0n muln0. +by rewrite ffactSS IH big_ord_recl subn0. +Qed. + Lemma ffact_gt0 n m : (0 < n ^_ m) = (m <= n). Proof. by elim: n m => [|n IHn] [|m] //=; rewrite ffactSS muln_gt0 IHn. Qed. |