Abstract natural integer powers can be a problem

[SnarkBoojum]

Here is an example where powers looking like n.+1 and n.+2 make ring fail:

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

From mathcomp.algebra_tactics Require Import ring.
Import Order.TTheory GRing.Theory.

Section Section.

Open Scope ring_scope.
Variable R: realDomainType.

Lemma sum_geom_second (x: R) n: (1 - x) * (\sum_(0 <= k < n.+1) x^k) = 1 - x^n.+1.
Proof.
elim: n => [|n Hn].
  rewrite unlock //=.
  by ring. (* Coq's ring doesn't work here *)
rewrite big_nat_recr //= mulrDr Hn. (* Hn doesn't work directly because of (1-x)* *)
Fail ring. (* mc.a-t's ring doesn't like abstract powers? *)
rewrite [in RHS]exprSz. (* let's give it a hand *)
by ring. (* now it works *)
Qed.

End Section.

[pi8027]

Indeed, the ring tactic does not support variables in exponents. There is an IJCAR 2020 paper by Anne Baanen about a (non-reflexive) ring tactic with better support for exponents. But it seems to me that this extension makes the problems undecidable. See #11.

[pi8027]

Duplicate of #11