From 020c051359aa05d1e22259b4739b9130ab65e472 Mon Sep 17 00:00:00 2001
From: Laurent Théry
Date: Mon, 30 Sep 2019 09:27:14 +0200
Subject: ffact as a product similar to fact_prod (#374)

Thanks!---
 mathcomp/ssreflect/binomial.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'mathcomp')

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.
 
-- 
cgit v1.2.3