diff options
| author | thery | 2020-06-24 16:00:24 +0200 |
|---|---|---|
| committer | thery | 2020-06-24 16:00:24 +0200 |
| commit | d7167e988d194e98157f7d7f837d933c7299ba2a (patch) | |
| tree | 32dac42c0afdbdb983e3dda22789c852dbac6be4 /mathcomp | |
| parent | f25ef67ad2f58a30f1e700da89811b193755d84e (diff) | |
simpler proof
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |