diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.closed_field.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.field.closed_field.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.closed_field.html | 470 |
1 files changed, 470 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.closed_field.html b/docs/htmldoc/mathcomp.field.closed_field.html new file mode 100644 index 0000000..2ee6879 --- /dev/null +++ b/docs/htmldoc/mathcomp.field.closed_field.html @@ -0,0 +1,470 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>mathcomp.field.closed_field</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.field.closed_field</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</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> + +<div class="doc"> + A proof that algebraically closed field enjoy quantifier elimination, + as described in + ``A formal quantifier elimination for algebraically closed fields'', + proceedings of Calculemus 2010, by Cyril Cohen and Assia Mahboubi + +<div class="paragraph"> </div> + + This file constructs an instance of quantifier elimination mixin, + (see the ssralg library) from the theory of polynomials with coefficients + is an algebraically closed field (see the polydiv library). + +<div class="paragraph"> </div> + + This file hence deals with the transformation of formulae part, which we + address by implementing one CPS style formula transformer per effective + operation involved in the proof of quantifier elimination. See the paper + for more details. +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing</span>.<br/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">Pdiv.Ring</span>.<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">PreClosedField</span>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="ClosedFieldQE"><span class="id" title="section">ClosedFieldQE</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="ClosedFieldQE.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.type"><span class="id" title="record">Field.type</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="ClosedFieldQE.axiom"><span class="id" title="variable">axiom</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ClosedField.axiom"><span class="id" title="definition">ClosedField.axiom</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="fF"><span class="id" title="abbreviation">fF</span></a> := (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="qf"><span class="id" title="abbreviation">qf</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_form"><span class="id" title="definition">qf_form</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rformula"><span class="id" title="definition">rformula</span></a> <span class="id" title="var">f</span>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="polyF"><span class="id" title="definition">polyF</span></a> := <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="eval_poly"><span class="id" title="definition">eval_poly</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) <span class="id" title="var">pf</span> := <br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#pf"><span class="id" title="variable">pf</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">c</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">q</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">q</span><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.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><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.ssralg.html#GRing.eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">c</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> <span class="id" title="keyword">else</span> 0.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rpoly"><span class="id" title="definition">rpoly</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) := <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="var">k</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="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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">c</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">q</span> <span class="id" title="keyword">then</span> <br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ <br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">m</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="var">m</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#793e3499c36e4c6595d810e871a5acdd"><span class="id" title="notation">.+2</span></a> <span class="id" title="keyword">else</span> <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.If"><span class="id" title="definition">GRing.If</span></a> (<span class="id" title="var">c</span> <a class="idref" href="mathcomp.algebra.ssralg.html#9cd193463422c398e84dc63b7a4a91e1"><span class="id" title="notation">==</span></a> 0) (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> 0%<span class="id" title="var">N</span>) (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> 1%<span class="id" title="var">N</span>)) <span class="id" title="var">q</span> <br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a>%<span class="id" title="var">N</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sizeTP"><span class="id" title="lemma">sizeTP</span></a> (<span class="id" title="var">k</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="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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">pf</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pf"><span class="id" title="variable">pf</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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pf"><span class="id" title="variable">pf</span></a>))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sizeT_qf"><span class="id" title="lemma">sizeT_qf</span></a> (<span class="id" title="var">k</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="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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <br/> + <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">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="isnull"><span class="id" title="definition">isnull</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</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="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="isnullP"><span class="id" title="lemma">isnullP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="isnull_qf"><span class="id" title="lemma">isnull_qf</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">b</span>, <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="lt_sizeT"><span class="id" title="definition">lt_sizeT</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">m</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a><a class="idref" href="mathcomp.field.closed_field.html#m"><span class="id" title="variable">m</span></a>)) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="lift"><span class="id" title="definition">lift</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.field.closed_field.html#ClosedFieldQE.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="keyword">let</span>: <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> <span class="id" title="var">q</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_lift"><span class="id" title="lemma">eval_lift</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</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.field.closed_field.html#ClosedFieldQE.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="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="lead_coefT"><span class="id" title="definition">lead_coefT</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) <span class="id" title="var">p</span> := <br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">c</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">q</span> <span class="id" title="keyword">then</span> <br/> + <a class="idref" href="mathcomp.field.closed_field.html#lead_coefT"><span class="id" title="definition">lead_coefT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">l</span> ⇒ <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.If"><span class="id" title="definition">GRing.If</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#l"><span class="id" title="variable">l</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9cd193463422c398e84dc63b7a4a91e1"><span class="id" title="notation">==</span></a> 0) (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="var">c</span>) (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#l"><span class="id" title="variable">l</span></a>)) <span class="id" title="var">q</span> <br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="lead_coefTP"><span class="id" title="lemma">lead_coefTP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <span class="id" title="keyword">∀</span> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>),<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lead_coefT"><span class="id" title="definition">lead_coefT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</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.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>)))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="lead_coefT_qf"><span class="id" title="lemma">lead_coefT_qf</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">c</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lead_coefT"><span class="id" title="definition">lead_coefT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="amulXnT"><span class="id" title="definition">amulXnT</span></a> (<span class="id" title="var">a</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">n</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a> :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#amulXnT"><span class="id" title="definition">amulXnT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</span></a> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_amulXnT"><span class="id" title="lemma">eval_amulXnT</span></a> (<span class="id" title="var">a</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">n</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>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#amulXnT"><span class="id" title="definition">amulXnT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</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.ssralg.html#GRing.eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</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.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ramulXnT"><span class="id" title="lemma">ramulXnT</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">n</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#amulXnT"><span class="id" title="definition">amulXnT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="sumpT"><span class="id" title="definition">sumpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">a</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">p'</span> <span class="id" title="keyword">then</span><br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">b</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">q'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Add"><span class="id" title="constructor">Add</span></a> <span class="id" title="var">a</span> <span class="id" title="var">b</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">)::(</span></a><a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> <span class="id" title="var">p'</span> <span class="id" title="var">q'</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">)</span></a><br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_sumpT"><span class="id" title="lemma">eval_sumpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><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.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><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.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rsumpT"><span class="id" title="lemma">rsumpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="mulpT"><span class="id" title="definition">mulpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">a</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> <span class="id" title="var">a</span>) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::(</span></a><a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <span class="id" title="var">p'</span> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">)</span></a>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_mulpT"><span class="id" title="lemma">eval_mulpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><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.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rpoly_map_mul"><span class="id" title="lemma">rpoly_map_mul</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">rt</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a>) : <br/> + <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rmulpT"><span class="id" title="lemma">rmulpT</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="opppT"><span class="id" title="definition">opppT</span></a> := <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a> (-1))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_opppT"><span class="id" title="lemma">eval_opppT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#opppT"><span class="id" title="definition">opppT</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="natmulpT"><span class="id" title="definition">natmulpT</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.NatConst"><span class="id" title="constructor">NatConst</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_natmulpT"><span class="id" title="lemma">eval_natmulpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">n</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>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#natmulpT"><span class="id" title="definition">natmulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="redivp_rec_loopT"><span class="id" title="definition">redivp_rec_loopT</span></a> (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) <span class="id" title="var">sq</span> <span class="id" title="var">cq</span> (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>)<br/> + (<span class="id" title="var">c</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>) (<span class="id" title="var">qq</span> <span class="id" title="var">r</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">n</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>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">n</span>}:=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sr</span> ⇒ <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sr"><span class="id" title="variable">sr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <br/> + <a class="idref" href="mathcomp.field.closed_field.html#lead_coefT"><span class="id" title="definition">lead_coefT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">lr</span> ⇒<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.field.closed_field.html#amulXnT"><span class="id" title="definition">amulXnT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lr"><span class="id" title="variable">lr</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sr"><span class="id" title="variable">sr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a>) <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">qq1</span> := <a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">r1</span> := <a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>)) (<a class="idref" href="mathcomp.field.closed_field.html#opppT"><span class="id" title="definition">opppT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)) <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n1</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loopT"><span class="id" title="definition">redivp_rec_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq1"><span class="id" title="variable">qq1</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r1"><span class="id" title="variable">r1</span></a> <span class="id" title="var">n1</span><br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq1"><span class="id" title="variable">qq1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r1"><span class="id" title="variable">r1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="redivp_rec_loop"><span class="id" title="definition">redivp_rec_loop</span></a> (<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.field.closed_field.html#ClosedFieldQE.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">sq</span> <span class="id" title="var">cq</span> <br/> + (<span class="id" title="var">k</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>) (<span class="id" title="var">qq</span> <span class="id" title="var">r</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.field.closed_field.html#ClosedFieldQE.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">n</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>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">n</span>} :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">m</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#81f8078534dcbb7e13a32d292f766525"><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.field.closed_field.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#81f8078534dcbb7e13a32d292f766525"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#81f8078534dcbb7e13a32d292f766525"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><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.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">)</span></a> <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">qq1</span> := <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</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.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.closed_field.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">r1</span> := <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</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.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <span class="id" title="tactic">in</span><br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n1</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loop"><span class="id" title="definition">redivp_rec_loop</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq1"><span class="id" title="variable">qq1</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r1"><span class="id" title="variable">r1</span></a> <span class="id" title="var">n1</span> <span class="id" title="keyword">else</span><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq1"><span class="id" title="variable">qq1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r1"><span class="id" title="variable">r1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="redivp_rec_loopTP"><span class="id" title="lemma">redivp_rec_loopTP</span></a> (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <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">∀</span> <span class="id" title="var">c</span> <span class="id" title="var">qq</span> <span class="id" title="var">r</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a><a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a><a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>) <br/> + <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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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/> + <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">∀</span> <span class="id" title="var">q</span> <span class="id" title="var">sq</span> <span class="id" title="var">cq</span> <span class="id" title="var">c</span> <span class="id" title="var">qq</span> <span class="id" title="var">r</span> <span class="id" title="var">n</span> <span class="id" title="var">e</span> <br/> + (<span class="id" title="var">d</span> := <a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loop"><span class="id" title="definition">redivp_rec_loop</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a>)<br/> + <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>),<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loopT"><span class="id" title="definition">redivp_rec_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>) <br/> + <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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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.1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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="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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="redivp_rec_loopT_qf"><span class="id" title="lemma">redivp_rec_loopT_qf</span></a> (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">sq</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>) (<span class="id" title="var">cq</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>)<br/> + (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">c</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>) (<span class="id" title="var">qq</span> <span class="id" title="var">r</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">n</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>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</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="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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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><br/> + <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loopT"><span class="id" title="definition">redivp_rec_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#cq"><span class="id" title="variable">cq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="redivpT"><span class="id" title="definition">redivpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) <br/> + (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> ⇒<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a><br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sq</span> ⇒<br/> + <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sp</span> ⇒<br/> + <a class="idref" href="mathcomp.field.closed_field.html#lead_coefT"><span class="id" title="definition">lead_coefT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">lq</span> ⇒<br/> + <a class="idref" href="mathcomp.field.closed_field.html#redivp_rec_loopT"><span class="id" title="definition">redivp_rec_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sq"><span class="id" title="variable">sq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lq"><span class="id" title="variable">lq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> 0 <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sp"><span class="id" title="variable">sp</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="redivp_rec_loopP"><span class="id" title="lemma">redivp_rec_loopP</span></a> (<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.field.closed_field.html#ClosedFieldQE.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">c</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>) (<span class="id" title="var">qq</span> <span class="id" title="var">r</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.field.closed_field.html#ClosedFieldQE.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">n</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>) :<br/> + <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.redivp_rec"><span class="id" title="definition">redivp_rec</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</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.field.closed_field.html#redivp_rec_loop"><span class="id" title="definition">redivp_rec_loop</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</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.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="redivpTP"><span class="id" title="lemma">redivpTP</span></a> (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">c</span> <span class="id" title="var">qq</span> <span class="id" title="var">r</span> <span class="id" title="var">e</span>, <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a><a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a><a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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> <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#c"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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> <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/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">e</span> (<span class="id" title="var">d</span> := <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.redivp"><span class="id" title="definition">redivp</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)),<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#redivpT"><span class="id" title="definition">redivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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.1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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="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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="redivpT_qf"><span class="id" title="lemma">redivpT_qf</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</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="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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</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="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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#33a541e60bd4a3e4dd9e7ab58beb75d4"><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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#redivpT"><span class="id" title="definition">redivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rmodpT"><span class="id" title="definition">rmodpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#redivpT"><span class="id" title="definition">redivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">d</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="rdivpT"><span class="id" title="definition">rdivpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span>:<a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#redivpT"><span class="id" title="definition">redivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">d</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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="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.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="rscalpT"><span class="id" title="definition">rscalpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</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="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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#redivpT"><span class="id" title="definition">redivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">d</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#d"><span class="id" title="variable">d</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.1</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="rdvdpT"><span class="id" title="definition">rdvdpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span>:<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</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.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#rmodpT"><span class="id" title="definition">rmodpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="rgcdp_loop"><span class="id" title="definition">rgcdp_loop</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">pp</span> <span class="id" title="var">qq</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.field.closed_field.html#ClosedFieldQE.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="keyword">struct</span> <span class="id" title="var">n</span>} :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rmodp"><span class="id" title="definition">rmodp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</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.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n1</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loop"><span class="id" title="definition">rgcdp_loop</span></a> <span class="id" title="var">n1</span> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> (<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rmodp"><span class="id" title="definition">rmodp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>)<br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rmodp"><span class="id" title="definition">rmodp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="rgcdp_loopT"><span class="id" title="definition">rgcdp_loopT</span></a> (<span class="id" title="var">pp</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) <span class="id" title="var">n</span> (<span class="id" title="var">qq</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#rmodpT"><span class="id" title="definition">rmodpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> <br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n1</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <br/> + <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#rmodpT"><span class="id" title="definition">rmodpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loopT"><span class="id" title="definition">rgcdp_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="var">n1</span>) <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a> <br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#rmodpT"><span class="id" title="definition">rmodpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pp"><span class="id" title="variable">pp</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a><br/> + )<br/> + ) <a class="idref" href="mathcomp.field.closed_field.html#qq"><span class="id" title="variable">qq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdp_loopP"><span class="id" title="lemma">rgcdp_loopP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <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/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">e</span>, <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loopT"><span class="id" title="definition">rgcdp_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loop"><span class="id" title="definition">rgcdp_loop</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdp_loopT_qf"><span class="id" title="lemma">rgcdp_loopT_qf</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">n</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>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/> + <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loopT"><span class="id" title="definition">rgcdp_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rgcdpT"><span class="id" title="definition">rgcdpT</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) <span class="id" title="var">k</span> (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">aux</span> <span class="id" title="var">p1</span> <span class="id" title="var">k</span> <span class="id" title="var">q1</span> := <a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> <br/> + (<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q1"><span class="id" title="variable">q1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ (<a class="idref" href="mathcomp.field.closed_field.html#rgcdp_loopT"><span class="id" title="definition">rgcdp_loopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q1"><span class="id" title="variable">q1</span></a>)) <a class="idref" href="mathcomp.field.closed_field.html#p1"><span class="id" title="variable">p1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#p1"><span class="id" title="variable">p1</span></a><br/> + <span class="id" title="tactic">in</span> (<a class="idref" href="mathcomp.field.closed_field.html#lt_sizeT"><span class="id" title="definition">lt_sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#aux"><span class="id" title="variable">aux</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#aux"><span class="id" title="variable">aux</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">)</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdpTP"><span class="id" title="lemma">rgcdpTP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <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/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpT"><span class="id" title="definition">rgcdpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgcdp"><span class="id" title="definition">rgcdp</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdpT_qf"><span class="id" title="lemma">rgcdpT_qf</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpT"><span class="id" title="definition">rgcdpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="rgcdpTs"><span class="id" title="definition">rgcdpTs</span></a> <span class="id" title="var">k</span> (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) : <a class="idref" href="mathcomp.field.closed_field.html#fF"><span class="id" title="abbreviation">fF</span></a> :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">p</span><a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a><span class="id" title="var">pr</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.field.closed_field.html#rgcdpTs"><span class="id" title="definition">rgcdpTs</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpT"><span class="id" title="definition">rgcdpT</span></a> <span class="id" title="var">p</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a>) <span class="id" title="var">pr</span> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdpTsP"><span class="id" title="lemma">rgcdpTsP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <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/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">ps</span> <span class="id" title="var">e</span>, <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpTs"><span class="id" title="definition">rgcdpTs</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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> <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">[</span></a>@<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgcdp"><span class="id" title="definition">rgcdp</span></a> <span class="id" title="var">_</span><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">/</span></a>0<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.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">)</span></a>))).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rseq_poly"><span class="id" title="definition">rseq_poly</span></a> <span class="id" title="var">ps</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgcdpTs_qf"><span class="id" title="lemma">rgcdpTs_qf</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="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.field.closed_field.html#rseq_poly"><span class="id" title="definition">rseq_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpTs"><span class="id" title="definition">rgcdpTs</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="rgdcop_recT"><span class="id" title="definition">rgdcop_recT</span></a> (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) <span class="id" title="var">k</span> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) <span class="id" title="var">n</span> :=<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">m</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span><br/> + <a class="idref" href="mathcomp.field.closed_field.html#rgcdpT"><span class="id" title="definition">rgcdpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sd</span> ⇒<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.field.closed_field.html#sd"><span class="id" title="variable">sd</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.field.closed_field.html#rgcdpT"><span class="id" title="definition">rgcdpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rdivpT"><span class="id" title="definition">rdivpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">r</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#rgdcop_recT"><span class="id" title="definition">rgdcop_recT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="var">m</span>)) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><br/> + )) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a><br/> + <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.field.closed_field.html#isnull"><span class="id" title="definition">isnull</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> <a class="idref" href="mathcomp.field.closed_field.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgdcop_recTP"><span class="id" title="lemma">rgdcop_recTP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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><br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">n</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcop_recT"><span class="id" title="definition">rgdcop_recT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>) <br/> + <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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgdcop_rec"><span class="id" title="definition">rgdcop_rec</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgdcop_recT_qf"><span class="id" title="lemma">rgdcop_recT_qf</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">n</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>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/> + <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcop_recT"><span class="id" title="definition">rgdcop_recT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rgdcopT"><span class="id" title="definition">rgdcopT</span></a> <span class="id" title="var">q</span> <span class="id" title="var">k</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcop_recT"><span class="id" title="definition">rgdcop_recT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgdcopTP"><span class="id" title="lemma">rgdcopTP</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <br/> + <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">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <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/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">e</span>, <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcopT"><span class="id" title="definition">rgdcopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#lift"><span class="id" title="definition">lift</span></a> (<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgdcop"><span class="id" title="definition">rgdcop</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)))).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgdcopT_qf"><span class="id" title="lemma">rgdcopT_qf</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</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.ssralg.html#GRing.formula"><span class="id" title="inductive">formula</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <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">∀</span> <span class="id" title="var">r</span>, <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.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="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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcopT"><span class="id" title="definition">rgdcopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ex_elim_seq"><span class="id" title="definition">ex_elim_seq</span></a> (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :=<br/> + (<a class="idref" href="mathcomp.field.closed_field.html#rgcdpTs"><span class="id" title="definition">rgcdpTs</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#rgdcopT"><span class="id" title="definition">rgdcopT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#sizeT"><span class="id" title="definition">sizeT</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">n</span> ⇒ <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Bool"><span class="id" title="constructor">Bool</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">N</span>)))) <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ex_elim_seqP"><span class="id" title="lemma">ex_elim_seqP</span></a> (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">gp</span> := (<a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">[</span></a>@<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgcdp"><span class="id" title="definition">rgcdp</span></a> <span class="id" title="var">_</span><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">/</span></a>0<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.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">(</span></a><span class="id" title="var">p</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">)</span></a>) <span class="id" title="tactic">in</span><br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.qf_eval"><span class="id" title="definition">qf_eval</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#ex_elim_seq"><span class="id" title="definition">ex_elim_seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a> <a class="idref" href="mathcomp.field.closed_field.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#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.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Ring.rgdcop"><span class="id" title="definition">rgdcop</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#gp"><span class="id" title="variable">gp</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1%<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>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ex_elim_seq_qf"><span class="id" title="lemma">ex_elim_seq_qf</span></a> (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.closed_field.html#polyF"><span class="id" title="definition">polyF</span></a>) :<br/> + <a class="idref" href="mathcomp.field.closed_field.html#rseq_poly"><span class="id" title="definition">rseq_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> <a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#ex_elim_seq"><span class="id" title="definition">ex_elim_seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="abstrX"><span class="id" title="definition">abstrX</span></a> (<span class="id" title="var">i</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>) (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Var"><span class="id" title="constructor">Var</span></a> <span class="id" title="var">n</span>) ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <span class="id" title="var">n</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 0<a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1<a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Opp"><span class="id" title="constructor">Opp</span></a> <span class="id" title="var">x</span>) ⇒ <a class="idref" href="mathcomp.field.closed_field.html#opppT"><span class="id" title="definition">opppT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">x</span>)<br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Add"><span class="id" title="constructor">Add</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) ⇒ <a class="idref" href="mathcomp.field.closed_field.html#sumpT"><span class="id" title="definition">sumpT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">x</span>) (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">y</span>)<br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) ⇒ <a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">x</span>) (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">y</span>)<br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.NatMul"><span class="id" title="constructor">NatMul</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span>) ⇒ <a class="idref" href="mathcomp.field.closed_field.html#natmulpT"><span class="id" title="definition">natmulpT</span></a> <span class="id" title="var">n</span> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">x</span>)<br/> + | (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Exp"><span class="id" title="constructor">Exp</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span>) ⇒ <span class="id" title="keyword">let</span> <span class="id" title="var">ax</span> := (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="var">x</span>) <span class="id" title="tactic">in</span><br/> + <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <span class="id" title="var">n</span> (<a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ax"><span class="id" title="variable">ax</span></a>) <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><br/> + | <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a><br/> + <span class="id" title="keyword">end</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="abstrXP"><span class="id" title="lemma">abstrXP</span></a> (<span class="id" title="var">i</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>) (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) :<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</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#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a>)<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.closed_field.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> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.eval"><span class="id" title="definition">eval</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#set_nth"><span class="id" title="definition">set_nth</span></a> 0 <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rabstrX"><span class="id" title="lemma">rabstrX</span></a> (<span class="id" title="var">i</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>) (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</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.field.closed_field.html#rpoly"><span class="id" title="definition">rpoly</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">tx</span> <span class="id" title="var">ty</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="abstrX_mulM"><span class="id" title="lemma">abstrX_mulM</span></a> (<span class="id" title="var">i</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.closed_field.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.closed_field.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="abstrX1"><span class="id" title="lemma">abstrX1</span></a> (<span class="id" title="var">i</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.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1) <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#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_poly_mulM"><span class="id" title="lemma">eval_poly_mulM</span></a> <span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.field.closed_field.html#mulpT"><span class="id" title="definition">mulpT</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.closed_field.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.closed_field.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eval_poly1"><span class="id" title="lemma">eval_poly1</span></a> <span class="id" title="var">e</span> : <a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1<a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><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> 1.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="abstrX_bigmul"><span class="id" title="abbreviation">abstrX_bigmul</span></a> := (<a class="idref" href="mathcomp.ssreflect.bigop.html#big_morph"><span class="id" title="lemma">big_morph</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX_mulM"><span class="id" title="lemma">abstrX_mulM</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.field.closed_field.html#abstrX1"><span class="id" title="lemma">abstrX1</span></a> <span class="id" title="var">_</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="eval_bigmul"><span class="id" title="abbreviation">eval_bigmul</span></a> := (<a class="idref" href="mathcomp.ssreflect.bigop.html#big_morph"><span class="id" title="lemma">big_morph</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly_mulM"><span class="id" title="lemma">eval_poly_mulM</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly1"><span class="id" title="lemma">eval_poly1</span></a> <span class="id" title="var">_</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="bigmap_id"><span class="id" title="abbreviation">bigmap_id</span></a> := (<a class="idref" href="mathcomp.ssreflect.bigop.html#big_map"><span class="id" title="lemma">big_map</span></a> <span class="id" title="var">_</span> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rseq_poly_map"><span class="id" title="lemma">rseq_poly_map</span></a> (<span class="id" title="var">x</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>) (<span class="id" title="var">ts</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>)) :<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.field.closed_field.html#ts"><span class="id" title="variable">ts</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.field.closed_field.html#rseq_poly"><span class="id" title="definition">rseq_poly</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#ts"><span class="id" title="variable">ts</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ex_elim"><span class="id" title="definition">ex_elim</span></a> (<span class="id" title="var">x</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>) (<span class="id" title="var">pqs</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</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.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>)) :=<br/> + <a class="idref" href="mathcomp.field.closed_field.html#ex_elim_seq"><span class="id" title="definition">ex_elim_seq</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#pqs"><span class="id" title="variable">pqs</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>) <br/> + (<a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Mul"><span class="id" title="constructor">Mul</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">/</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Const"><span class="id" title="constructor">Const</span></a> 1<a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">(</span></a><span class="id" title="var">q</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pqs"><span class="id" title="variable">pqs</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.bigop.html#30705c25db0a97e8b1b08168f9199b27"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.closed_field.html#q"><span class="id" title="variable">q</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ex_elim_qf"><span class="id" title="lemma">ex_elim_qf</span></a> (<span class="id" title="var">x</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>) (<span class="id" title="var">pqs</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</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.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>)) : <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.dnf_rterm"><span class="id" title="definition">dnf_rterm</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pqs"><span class="id" title="variable">pqs</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.field.closed_field.html#qf"><span class="id" title="abbreviation">qf</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#ex_elim"><span class="id" title="definition">ex_elim</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.field.closed_field.html#pqs"><span class="id" title="variable">pqs</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="holds_conj"><span class="id" title="lemma">holds_conj</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">i</span> <span class="id" title="var">x</span> <span class="id" title="var">ps</span>, <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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/> + <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.ssralg.html#GRing.holds"><span class="id" title="definition">holds</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#set_nth"><span class="id" title="definition">set_nth</span></a> 0 <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a> ⇒ <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.And"><span class="id" title="constructor">And</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9cd193463422c398e84dc63b7a4a91e1"><span class="id" title="notation">==</span></a> 0)) <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.True"><span class="id" title="abbreviation">True</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a>)<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">(</span></a>@<a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">)^~</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="holds_conjn"><span class="id" title="lemma">holds_conjn</span></a> (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">i</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>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>) (<span class="id" title="var">ps</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a>)) :<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (@<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.rterm"><span class="id" title="definition">rterm</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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/> + <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.ssralg.html#GRing.holds"><span class="id" title="definition">holds</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#set_nth"><span class="id" title="definition">set_nth</span></a> 0 <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE.F"><span class="id" title="variable">F</span></a> ⇒ <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.And"><span class="id" title="constructor">And</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e55bf22d80797140224ba2d3a71d012f"><span class="id" title="notation">!=</span></a> 0)) <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.True"><span class="id" title="abbreviation">True</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">p</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><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.field.closed_field.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.closed_field.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.field.closed_field.html#eval_poly"><span class="id" title="definition">eval_poly</span></a> <a class="idref" href="mathcomp.field.closed_field.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.field.closed_field.html#abstrX"><span class="id" title="definition">abstrX</span></a> <a class="idref" href="mathcomp.field.closed_field.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.field.closed_field.html#ps"><span class="id" title="variable">ps</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/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="holds_ex_elim"><span class="id" title="lemma">holds_ex_elim</span></a>: <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.valid_QE_proj"><span class="id" title="definition">GRing.valid_QE_proj</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ex_elim"><span class="id" title="definition">ex_elim</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="wf_ex_elim"><span class="id" title="lemma">wf_ex_elim</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.wf_QE_proj"><span class="id" title="definition">GRing.wf_QE_proj</span></a> <a class="idref" href="mathcomp.field.closed_field.html#ex_elim"><span class="id" title="definition">ex_elim</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="closed_fields_QEMixin"><span class="id" title="definition">closed_fields_QEMixin</span></a> := <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.QEdecFieldMixin"><span class="id" title="definition">QEdecFieldMixin</span></a> <a class="idref" href="mathcomp.field.closed_field.html#wf_ex_elim"><span class="id" title="lemma">wf_ex_elim</span></a> <a class="idref" href="mathcomp.field.closed_field.html#holds_ex_elim"><span class="id" title="lemma">holds_ex_elim</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.closed_field.html#ClosedFieldQE"><span class="id" title="section">ClosedFieldQE</span></a>.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file |