From 31978e486f48b902d18c5f508e34bc016d7f47b8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 25 Aug 2020 00:14:50 +0200
Subject: Adding commr_horner lemma

---
 mathcomp/algebra/poly.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e83bc09..a33788d 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1093,6 +1093,12 @@ Proof. by rewrite /comm_poly !hornerC !simp. Qed.
 Lemma comm_polyX x : comm_poly 'X x.
 Proof. by rewrite /comm_poly !hornerX. Qed.
 
+Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b].
+Proof.
+move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _.
+by apply: commrM => //; apply: commrX.
+Qed.
+
 Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x].
 Proof.
 move=> comm_qx.
-- 
cgit v1.2.3