diff options
| author | Georges Gonthier | 2019-05-08 09:38:02 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-08 09:38:02 +0200 |
| commit | 51b9988f608625c60184dbe90133d64cdaa2a1f9 (patch) | |
| tree | 5315fbaebdbeca10f6a9ffba448ea424d16252b3 /mathcomp/ssreflect/binomial.v | |
| parent | 02830d7cf24f9198d5e7cb81843d6ca5cb69f68a (diff) | |
| parent | 6c4382c69e72b81fb7e81b0b753e5d3c83b1064a (diff) | |
Merge pull request #344 from soraros/ssrnat-remove-arith-lemmas
remove dependence on Arith lemmas
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index c260105..06774ff 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -45,7 +45,7 @@ transitivity (\sum_(1 <= i < n.+1) \sum_(1 <= k < n.+1) (p ^ k %| i)). by apply: andb_idr => /dvdn_leq/(leq_trans (ltn_expl _ (prime_gt1 _)))->. by rewrite exchange_big_nat; apply: eq_bigr => i _; rewrite divn_count_dvd. Qed. - + Theorem Wilson p : p > 1 -> prime p = (p %| ((p.-1)`!).+1). Proof. have dFact n: 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i. @@ -310,7 +310,7 @@ Qed. Lemma subn_exp m n k : m ^ k - n ^ k = (m - n) * (\sum_(i < k) m ^ (k.-1 -i) * n ^ i). Proof. -case: k => [|k]; first by rewrite big_ord0. +case: k => [|k]; first by rewrite big_ord0 muln0. rewrite mulnBl !big_distrr big_ord_recl big_ord_recr /= subn0 muln1. rewrite subnn mul1n -!expnS subnDA; congr (_ - _); apply: canRL (addnK _) _. congr (_ + _); apply: eq_bigr => i _. @@ -543,4 +543,3 @@ by apply: val_inj; congr (_ :: _); apply: val_inj; rewrite /= -{1}def_n addnK. Qed. End Combinations. - |