From d7167e988d194e98157f7d7f837d933c7299ba2a Mon Sep 17 00:00:00 2001
From: thery
Date: Wed, 24 Jun 2020 16:00:24 +0200
Subject: simpler proof

---
 mathcomp/ssreflect/bigop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 5f1b7d7..c6b2dfc 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1823,7 +1823,7 @@ Lemma prod_nat_const n : \prod_(i in A) n = n ^ #|A|.
 Proof. by rewrite big_const -Monoid.iteropE. Qed.
 
 Lemma sum_nat_const_nat n1 n2 n : \sum_(n1 <= i < n2) n = (n2 - n1) * n.
-Proof. by rewrite big_const_nat; elim: (_ - _) => //= ? ->. Qed.
+Proof. by rewrite big_const_nat iter_addn_0 mulnC. Qed.
 
 Lemma prod_nat_const_nat n1 n2 n : \prod_(n1 <= i < n2) n = n ^ (n2 - n1).
 Proof. by rewrite big_const_nat -Monoid.iteropE. Qed.
-- 
cgit v1.2.3