htmldoc regenerated

1 files changed, 78 insertions, 79 deletions

diff --git a/docs/htmldoc/mathcomp.algebra.polyXY.html b/docs/htmldoc/mathcomp.algebra.polyXY.html
index 5506005..53a0eb8 100644
--- a/docs/htmldoc/mathcomp.algebra.polyXY.html
+++ b/docs/htmldoc/mathcomp.algebra.polyXY.html
@@ -21,7 +21,6 @@
 <div class="code">
 <span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
 &nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
-<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
 
 <br/>
 </div>
@@ -67,9 +66,9 @@
 <br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="123da97e9d81425c68e579737576ac03"><span class="id" title="notation">&quot;</span></a>'Y" := <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a> : <span class="id" title="var">ring_scope</span>.<br/>
-<span class="id" title="keyword">Notation</span> <a name="f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">&quot;</span></a>p ^:P" := (<span class="id" title="var">p</span> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "p ^:P") : <span class="id" title="var">ring_scope</span>.<br/>
-<span class="id" title="keyword">Notation</span> <a name="7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">&quot;</span></a>p .[ x , y ]" := (<span class="id" title="var">p</span><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><span class="id" title="var">x</span><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">].[</span></a><span class="id" title="var">y</span><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">&quot;</span></a>'Y" := <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a> : <span class="id" title="var">ring_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">&quot;</span></a>p ^:P" := (<span class="id" title="var">p</span> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "p ^:P") : <span class="id" title="var">ring_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">&quot;</span></a>p .[ x , y ]" := (<span class="id" title="var">p</span><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><span class="id" title="var">x</span><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">].[</span></a><span class="id" title="var">y</span><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "p .[ x ,  y ]") : <span class="id" title="var">ring_scope</span>.<br/>
 
 <br/>
@@ -77,90 +76,90 @@
 
 <br/>
 <span class="id" title="keyword">Variable</span> <a name="PolyXY_Ring.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>.<br/>
-<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a>) (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a>) (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Fact</span> <a name="swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>.  <br/>
-<span class="id" title="keyword">Definition</span> <a name="swapXY_def"><span class="id" title="definition">swapXY_def</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Definition</span> <a name="swapXY"><span class="id" title="definition">swapXY</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_def"><span class="id" title="definition">swapXY_def</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_unlockable</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">unlockable</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">fun</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Fact</span> <a name="swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>.  <br/>
+<span class="id" title="keyword">Definition</span> <a name="swapXY_def"><span class="id" title="definition">swapXY_def</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="swapXY"><span class="id" title="definition">swapXY</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_def"><span class="id" title="definition">swapXY_def</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_unlockable</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">unlockable</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">fun</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="sizeY"><span class="id" title="definition">sizeY</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := <a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">max_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#2e8f487d341e1ab4c6af2ac15a318eda"><span class="id" title="notation">)</span></a>.<br/>
-<span class="id" title="keyword">Definition</span> <a name="poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">)</span></a>.<br/>
-<span class="id" title="keyword">Definition</span> <a name="poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">)</span></a>.<br/>
-<span class="id" title="keyword">Definition</span> <a name="sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a>.<br/>
-<span class="id" title="keyword">Definition</span> <a name="div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="sizeY"><span class="id" title="definition">sizeY</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">max_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_polyC"><span class="id" title="lemma">swapXY_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_polyC"><span class="id" title="lemma">swapXY_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_X"><span class="id" title="lemma">swapXY_X</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">Y</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_X"><span class="id" title="lemma">swapXY_X</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_Y"><span class="id" title="lemma">swapXY_Y</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#123da97e9d81425c68e579737576ac03"><span class="id" title="notation">Y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_Y"><span class="id" title="lemma">swapXY_Y</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a>.<br/>
  
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="swapXY_is_additive"><span class="id" title="lemma">swapXY_is_additive</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.additive"><span class="id" title="abbreviation">additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
  <span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_addf</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.Additive"><span class="id" title="abbreviation">Additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_additive"><span class="id" title="lemma">swapXY_is_additive</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="coef_swapXY"><span class="id" title="lemma">coef_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">)`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_j</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_i</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="coef_swapXY"><span class="id" title="lemma">coef_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">)`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_j</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXYK"><span class="id" title="lemma">swapXYK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXYK"><span class="id" title="lemma">swapXYK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_map_polyC"><span class="id" title="lemma">swapXY_map_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_map_polyC"><span class="id" title="lemma">swapXY_map_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_eq0"><span class="id" title="lemma">swapXY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_eq0"><span class="id" title="lemma">swapXY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="swapXY_is_multiplicative"><span class="id" title="lemma">swapXY_is_multiplicative</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.multiplicative"><span class="id" title="abbreviation">multiplicative</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
 <span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_rmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.AddRMorphism"><span class="id" title="abbreviation">AddRMorphism</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_multiplicative"><span class="id" title="lemma">swapXY_is_multiplicative</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_is_scalable"><span class="id" title="lemma">swapXY_is_scalable</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable_for"><span class="id" title="abbreviation">scalable_for</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c42c5cb909c30537f9f6acfcf01cf7e1"><span class="id" title="notation">\;</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d5d4e2467843f67554f1a8a22d125de9"><span class="id" title="notation">R</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_is_scalable"><span class="id" title="lemma">swapXY_is_scalable</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable_for"><span class="id" title="abbreviation">scalable_for</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#11ebad41b70994075d9152ef8d0a15b3"><span class="id" title="notation">\;</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">R</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/>
  <span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_linear</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.AddLinear"><span class="id" title="abbreviation">AddLinear</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_scalable"><span class="id" title="lemma">swapXY_is_scalable</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_lrmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#8900f6ae77a86586561e15965d5870c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8900f6ae77a86586561e15965d5870c7"><span class="id" title="notation">lrmorphism</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8900f6ae77a86586561e15965d5870c7"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8900f6ae77a86586561e15965d5870c7"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_lrmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">lrmorphism</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_comp_poly"><span class="id" title="lemma">swapXY_comp_poly</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#f734b1360ed3aede5055701a3bc465fd"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_comp_poly"><span class="id" title="lemma">swapXY_comp_poly</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="max_size_coefXY"><span class="id" title="lemma">max_size_coefXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9625b440a0052f6dbfd015f5bb8b5125"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="max_size_coefXY"><span class="id" title="lemma">max_size_coefXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="max_size_lead_coefXY"><span class="id" title="lemma">max_size_lead_coefXY</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="max_size_lead_coefXY"><span class="id" title="lemma">max_size_lead_coefXY</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="max_size_evalX"><span class="id" title="lemma">max_size_evalX</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="max_size_evalX"><span class="id" title="lemma">max_size_evalX</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">).-1</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="max_size_evalC"><span class="id" title="lemma">max_size_evalC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="max_size_evalC"><span class="id" title="lemma">max_size_evalC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="sizeYE"><span class="id" title="lemma">sizeYE</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sizeYE"><span class="id" title="lemma">sizeYE</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="sizeY_eq0"><span class="id" title="lemma">sizeY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0%<span class="id" title="var">N</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sizeY_eq0"><span class="id" title="lemma">sizeY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0%<span class="id" title="var">N</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="sizeY_mulX"><span class="id" title="lemma">sizeY_mulX</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sizeY_mulX"><span class="id" title="lemma">sizeY_mulX</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XaY"><span class="id" title="lemma">swapXY_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XaY"><span class="id" title="lemma">swapXY_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XmY"><span class="id" title="lemma">swapXY_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XmY"><span class="id" title="lemma">swapXY_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="poly_XaY0"><span class="id" title="lemma">poly_XaY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="poly_XaY0"><span class="id" title="lemma">poly_XaY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="poly_XmY0"><span class="id" title="lemma">poly_XmY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="poly_XmY0"><span class="id" title="lemma">poly_XmY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
  
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring"><span class="id" title="section">PolyXY_Ring</span></a>.<br/>
@@ -168,30 +167,30 @@
 <br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="swapXY_map"><span class="id" title="lemma">swapXY_map</span></a> (<span class="id" title="var">R</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#6566b94c06c342b0768c3d2d73badf6e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6566b94c06c342b0768c3d2d73badf6e"><span class="id" title="notation">additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6566b94c06c342b0768c3d2d73badf6e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">u</span> :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#f"><span class="id" title="variable">f</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="swapXY_map"><span class="id" title="lemma">swapXY_map</span></a> (<span class="id" title="var">R</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">}</span></a>) <span class="id" title="var">u</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#f"><span class="id" title="variable">f</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Section</span> <a name="PolyXY_ComRing"><span class="id" title="section">PolyXY_ComRing</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Variable</span> <a name="PolyXY_ComRing.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>.<br/>
-<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="horner_swapXY"><span class="id" title="lemma">horner_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="horner_swapXY"><span class="id" title="lemma">horner_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="horner_polyC"><span class="id" title="lemma">horner_polyC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="horner_polyC"><span class="id" title="lemma">horner_polyC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="horner2_swapXY"><span class="id" title="lemma">horner2_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="horner2_swapXY"><span class="id" title="lemma">horner2_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XaY"><span class="id" title="lemma">horner_poly_XaY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XaY"><span class="id" title="lemma">horner_poly_XaY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XmY"><span class="id" title="lemma">horner_poly_XmY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XmY"><span class="id" title="lemma">horner_poly_XmY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing"><span class="id" title="section">PolyXY_ComRing</span></a>.<br/>
@@ -201,49 +200,49 @@
 
 <br/>
 <span class="id" title="keyword">Variable</span> <a name="PolyXY_Idomain.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/>
-<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="size_poly_XaY"><span class="id" title="lemma">size_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_poly_XaY"><span class="id" title="lemma">size_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="poly_XaY_eq0"><span class="id" title="lemma">poly_XaY_eq0</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="poly_XaY_eq0"><span class="id" title="lemma">poly_XaY_eq0</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="size_poly_XmY"><span class="id" title="lemma">size_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_poly_XmY"><span class="id" title="lemma">size_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="poly_XmY_eq0"><span class="id" title="lemma">poly_XmY_eq0</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="poly_XmY_eq0"><span class="id" title="lemma">poly_XmY_eq0</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="lead_coef_poly_XaY"><span class="id" title="lemma">lead_coef_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lead_coef_poly_XaY"><span class="id" title="lemma">lead_coef_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="sub_annihilant_in_ideal"><span class="id" title="lemma">sub_annihilant_in_ideal</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a><br/>
-&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><br/>
-&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a><br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="sub_annihilantP"><span class="id" title="lemma">sub_annihilantP</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="sub_annihilant_neq0"><span class="id" title="lemma">sub_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sub_annihilant_neq0"><span class="id" title="lemma">sub_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0.<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="div_annihilant_in_ideal"><span class="id" title="lemma">div_annihilant_in_ideal</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}}</span></a><br/>
-&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><br/>
-&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#7fe0b4b004984abb7cb175c362f61dea"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}}</span></a><br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="div_annihilant_neq0"><span class="id" title="lemma">div_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a>0<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="div_annihilant_neq0"><span class="id" title="lemma">div_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a>0<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain"><span class="id" title="section">PolyXY_Idomain</span></a>.<br/>
@@ -252,35 +251,35 @@
 <span class="id" title="keyword">Section</span> <a name="PolyXY_Field"><span class="id" title="section">PolyXY_Field</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Variables</span> (<a name="PolyXY_Field.F"><span class="id" title="variable">F</span></a> <a name="PolyXY_Field.E"><span class="id" title="variable">E</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="PolyXY_Field.F"><span class="id" title="variable">F</span></a> <a name="PolyXY_Field.E"><span class="id" title="variable">E</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>).<br/>
 
 <br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="div_annihilantP"><span class="id" title="lemma">div_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="div_annihilantP"><span class="id" title="lemma">div_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="map_sub_annihilantP"><span class="id" title="lemma">map_sub_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="map_sub_annihilantP"><span class="id" title="lemma">map_sub_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="map_div_annihilantP"><span class="id" title="lemma">map_div_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="map_div_annihilantP"><span class="id" title="lemma">map_div_annihilantP</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="root_annihilant"><span class="id" title="lemma">root_annihilant</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> (<span class="id" title="var">pEx</span> := <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pFtoE"><span class="id" title="abbreviation">pFtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a>) :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">r</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="root_annihilant"><span class="id" title="lemma">root_annihilant</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> (<span class="id" title="var">pEx</span> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pFtoE"><span class="id" title="abbreviation">pFtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">r</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="algebraic_root_polyXY"><span class="id" title="lemma">algebraic_root_polyXY</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">let</span> <span class="id" title="var">pEx</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#b033a3d34e421a2439563f5ffdab0b9b"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">let</span> <span class="id" title="var">pEx</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/>
  
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field"><span class="id" title="section">PolyXY_Field</span></a>.<br/>