horner form in ring_nf

Stream: mathlib4

[Bhavik Mehta]

Has ring_nf lost the ability to rewrite into horner normal form? I found this useful as a non-terminal use of ring_nf, as well as for evaluation. I can't see it in the docs or source for ring_nf in mathlib4

[Scott Morrison]

Yes.

[Mario Carneiro]

It no longer uses horner normal form internally, but it could rewrite into horner form if desired for other reasons