diff options
| author | Cyril Cohen | 2020-11-13 15:00:55 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-13 15:00:55 +0100 |
| commit | 1a098263b335ccc4cf72880662dccbe79185a8ab (patch) | |
| tree | 057f0c89a13a19aae6624bd1f235f9a3530b7f57 /mathcomp/ssreflect/binomial.v | |
| parent | 903f12374f8b388b8f28da6cad06724ae0bf5075 (diff) | |
| parent | 2f906481423530b03f21ff605aaee3f281131608 (diff) | |
Merge pull request #646 from pi8027/rename-eq_sorted
Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 836c323..cd3ec87 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -468,7 +468,7 @@ have ft_m: #|f_t t| = m. rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj). exact: (sorted_uniq ltn_trans ltnn). rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=. -apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y. +apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y. by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *. Qed. |