diff options
| author | Kazuhiko Sakaguchi | 2020-05-16 09:02:13 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-05-16 09:30:39 +0900 |
| commit | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (patch) | |
| tree | 3f3f5a094547ae1166a21cb7c5350c7e5a87404a /mathcomp/ssreflect/binomial.v | |
| parent | 35bd8708dacfb508f896d957d7b1189ca7decb3e (diff) | |
A few more revisions
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 24c2adf..d419745 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -80,8 +80,7 @@ have vFpV i: i != Fp0 -> mFp (vFp i) i = Fp1. rewrite coprime_sym prime_coprime //; apply/negP=> /(dvdn_leq i_gt0). by rewrite leqNgt ltn_ord. have vFp0 i: i != Fp0 -> vFp i != Fp0. - move/vFpV=> inv_i; apply/eqP=> vFp0. - by have:= congr1 val inv_i; rewrite vFp0 /= mod0n. + by move/vFpV; apply/contra_eq_neq => ->; rewrite -val_eqE /= mul0n mod0n. have vFpK: {in predC1 Fp0, involutive vFp}. move=> i n0i; rewrite /= -[vFp _]mFp1r -(vFpV _ n0i) mFpA. by rewrite vFpV (vFp0, mFp1). @@ -113,7 +112,7 @@ rewrite [mFpM _ _]mFp1 (bigD1 Fpn1) -?mFpA -/mFpM; last first. by rewrite [ltv _]ltn_neqAle vFpId eqxx orbT eq_sym eqF1n1. rewrite (reindex_onto vFp vFp) -/mFpM => [|i]; last by do 3!case/andP; auto. rewrite (eq_bigl (xpredD1 ltv Fp0)) => [|i]; last first. - rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt andbA -ltnNge. + rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt -ltnNge. have [->|ni0] := eqVneq i; last by rewrite vFpK // eqxx vFp0. by case: eqP => // ->; rewrite !andbF. rewrite -{2}[mFp]/mFpM -[mFpM _ _]big_split -/mFpM. |