Slow BarrettReduction?

Surely

 destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond];
        eauto using Z.lt_gt with zarith.

was not taking 95 seconds when we first wrote that line, and something is going wrong?

Originally posted by @JasonGross in coq/coq#18818 (comment)

fiat-crypto/src/Arithmetic/BarrettReduction.v

Lines 103 to 104 in a8816f0

    
           { destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond]; 
        
               eauto using Z.lt_gt with zarith. }

Is it just the bench machine that is slow, I see
0m15.19s | 520360 ko | Arithmetic/BarrettReduction.vo
in 9584e6c

CI dev says
1m38.92s | 774816 ko | Arithmetic/BarrettReduction.vo
but I can't find logs that stretch back far enough to see if it was always that way.

	{ destruct q_nice_strong with (b:=b) (k:=k) (m:=mu) (offset:=1) (a:=x) (n:=M) as [cond Hcond];
	eauto using Z.lt_gt with zarith. }