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

---
 CHANGELOG_UNRELEASED.md | 2 ++
 mathcomp/algebra/poly.v | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ea671b5..245b505 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -38,6 +38,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `scalar_mx_is_diag`, `is_scalar_mx_is_diag`, `scalar_mx_is_trig` and
   `is_scalar_mx_is_trig`.
 
+- in `poly.v`, new lemma `commr_horner`.
+
 ### Changed
 
 - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
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