diff options
| author | Cyril Cohen | 2020-06-24 18:17:03 +0200 |
|---|---|---|
| committer | GitHub | 2020-06-24 18:17:03 +0200 |
| commit | 85c876ba8db646af6258445ee6838b184eaaedb3 (patch) | |
| tree | 41b6c72b82908f99ae29a51f0a395555a870f130 /mathcomp | |
| parent | 6ad37558afefbad4954214c439cdc41cafdc829b (diff) | |
| parent | d7167e988d194e98157f7d7f837d933c7299ba2a (diff) | |
Merge pull request #539 from thery/sum_nat_const
simpler proof of sum_nat_const_nat in bigop.v
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. |