From c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 27 Feb 2019 17:31:35 +0100
Subject: Add extra eta lemmas for the under tactic

Related: coq/coq#9651
---
 mathcomp/algebra/matrix.v | 5 +++++
 mathcomp/algebra/poly.v   | 4 ++++
 2 files changed, 9 insertions(+)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 3b12802..2580741 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -232,8 +232,13 @@ rewrite /fun_of_matrix; split=> [/= eqAB | -> //].
 by apply/val_inj/ffunP=> [[i j]]; apply: eqAB.
 Qed.
 
+Lemma eq_mx k F1 F2 : (F1 =2 F2) -> matrix_of_fun k F1 = matrix_of_fun k F2.
+Proof. by move=> eq_F; apply/matrixP => i j; rewrite !mxE eq_F. Qed.
+
 End MatrixDef.
 
+Arguments eq_mx {R m n k} [F1] F2 eq_F12.
+
 Bind Scope ring_scope with matrix.
 
 Notation "''M[' R ]_ ( m , n )" := (matrix R m n) (only parsing): type_scope.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 702dfc4..e0feecf 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1673,6 +1673,9 @@ apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->.
 by rewrite horner0 simp.
 Qed.
 
+Lemma eq_poly n E1 E2 : E1 =1 E2 -> poly n E1 = poly n E2.
+Proof. by move=> E; rewrite !poly_def; apply: eq_bigr => i _; rewrite E. Qed.
+
 End PolynomialTheory.
 
 Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver.
@@ -1695,6 +1698,7 @@ Arguments rootPt {R p x}.
 Arguments unity_rootP {R n z}.
 Arguments polyOverP {R S0 addS kS p}.
 Arguments polyC_inj {R} [x1 x2] eq_x12P.
+Arguments eq_poly {R n} [E1] E2 eq_E12.
 
 Canonical polynomial_countZmodType (R : countRingType) :=
   [countZmodType of polynomial R].
-- 
cgit v1.2.3