diff options
| author | Laurent Théry | 2019-09-30 09:27:14 +0200 |
|---|---|---|
| committer | Assia Mahboubi | 2019-09-30 09:27:14 +0200 |
| commit | 020c051359aa05d1e22259b4739b9130ab65e472 (patch) | |
| tree | 3d70e7d4689e50d79b98b62e724adefb97b02bce /mathcomp | |
| parent | d3dc7c337f2f031cec57d1f8804d59662e36ecfb (diff) | |
ffact as a product similar to fact_prod (#374)
Thanks!
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |