From 9ac21ad77cee351be1dabd1d8f2aef31fef141fe Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 28 Jun 2024 14:05:47 +0200 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1223 --- theories/abel.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/abel.v b/theories/abel.v index cf6694d..e13017d 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -1300,7 +1300,7 @@ rewrite -!sum1_count; pose pR : {poly algR} := poly_example ^^ ratr. have pR0 : pR != 0 by rewrite map_poly_eq0. suff cR : (\sum_(j <- example_roots | j \is Num.real) 1)%N = 3%N. have := size_example_roots; rewrite -sum1_size (bigID (mem Num.real))/=. - by rewrite cR => -[->]. + by rewrite cR => -[]. rewrite -big_filter (perm_big (map algRval (rootsR pR))); last first. rewrite uniq_perm ?filter_uniq ?example_roots_uniq//. by rewrite (map_inj_uniq (fmorph_inj _)) uniq_roots.