From mathcomp Require Import all_ssreflect all_algebra ssralg ssrint ssrnum.

From mathcomp.analysis Require Import reals.

From mathcomp.algebra_tactics Require Import ring.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory.

Local Open Scope ring_scope.

Import GRing.

Section BadHornerE.

Variable RR: realType.

Definition RX := { poly RR }.
Definition Psum := (4 *: 'X^3 - 3 *: 'X + 1) : RX.
Variable a: RR.

Lemma nameless: Psum.[a] == 4 * a^+ 3 - 3 * a + 1.
Proof.
(* rewrite !hornerE. should be enough, I think, but gives an awful result *)
by rewrite !hornerD hornerN !hornerZ horner_exp hornerX hornerC.
Qed.

End BadHornerE.