htmldoc regenerated

author: Enrico Tassi 2019-05-22 13:43:08 +0200
committer: Enrico Tassi 2019-05-22 15:34:14 +0200
commit: 748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree: fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.solvable.alt.html
parent: 415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
1 files changed, 41 insertions, 42 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.alt.html b/docs/htmldoc/mathcomp.solvable.alt.html
index dd87d49..f94a27f 100644
--- a/docs/htmldoc/mathcomp.solvable.alt.html
+++ b/docs/htmldoc/mathcomp.solvable.alt.html
@@ -21,7 +21,6 @@
 <div class="code">
 <span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
 &nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
-<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
 
 <br/>
 </div>
@@ -42,16 +41,16 @@
 <span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin"><span class="id" title="definition">FinGroup.Mixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbA"><span class="id" title="lemma">addbA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addFb"><span class="id" title="lemma">addFb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_baseGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.BaseFinGroupType"><span class="id" title="abbreviation">BaseFinGroupType</span></a> <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="mathcomp.solvable.alt.html#bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">boolGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType"><span class="id" title="abbreviation">FinGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin"><span class="id" title="definition">FinGroup.Mixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addbA"><span class="id" title="lemma">addbA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addFb"><span class="id" title="lemma">addFb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_baseGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.BaseFinGroupType"><span class="id" title="abbreviation">BaseFinGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="mathcomp.solvable.alt.html#bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">boolGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType"><span class="id" title="abbreviation">FinGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Section</span> <a name="SymAltDef"><span class="id" title="section">SymAltDef</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Variable</span> <a name="SymAltDef.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
-<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a>).<br/>
 
 <br/>
 </div>
@@ -60,132 +59,132 @@
  Definitions of the alternate groups and some Properties * 
 </div>
 <div class="code">
-<span class="id" title="keyword">Definition</span> <a name="Sym"><span class="id" title="definition">Sym</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Sym"><span class="id" title="definition">Sym</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Sym_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Sym_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sign_morph</span> := @<a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in2W"><span class="id" title="lemma">in2W</span></a> (@<a class="idref" href="mathcomp.fingroup.perm.html#odd_permM"><span class="id" title="lemma">odd_permM</span></a> <span class="id" title="var">_</span>)).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sign_morph</span> := @<a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#in2W"><span class="id" title="lemma">in2W</span></a> (@<a class="idref" href="mathcomp.fingroup.perm.html#odd_permM"><span class="id" title="lemma">odd_permM</span></a> <span class="id" title="var">_</span>)).<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="Alt"><span class="id" title="definition">Alt</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">(</span></a>@<a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Alt"><span class="id" title="definition">Alt</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">(</span></a>@<a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">)</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Alt_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Alt_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_even"><span class="id" title="lemma">Alt_even</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.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.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</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="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.solvable.alt.html#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_even"><span class="id" title="lemma">Alt_even</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_subset"><span class="id" title="lemma">Alt_subset</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_subset"><span class="id" title="lemma">Alt_subset</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_normal"><span class="id" title="lemma">Alt_normal</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_normal"><span class="id" title="lemma">Alt_normal</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_norm"><span class="id" title="lemma">Alt_norm</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_norm"><span class="id" title="lemma">Alt_norm</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Let</span> <a name="SymAltDef.n"><span class="id" title="variable">n</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+<span class="id" title="keyword">Let</span> <a name="SymAltDef.n"><span class="id" title="variable">n</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_index"><span class="id" title="lemma">Alt_index</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.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="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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> 2.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_index"><span class="id" title="lemma">Alt_index</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 2.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="card_Sym"><span class="id" title="lemma">card_Sym</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_Sym"><span class="id" title="lemma">card_Sym</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="card_Alt"><span class="id" title="lemma">card_Alt</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.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> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_Alt"><span class="id" title="lemma">card_Alt</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Sym_trans"><span class="id" title="lemma">Sym_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Sym_trans"><span class="id" title="lemma">Sym_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="Alt_trans"><span class="id" title="lemma">Alt_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#b870774a3786e6850cf468108b4e1ee5"><span class="id" title="notation">.-2</span></a> <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Alt_trans"><span class="id" title="lemma">Alt_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#b9f3db5365f11e72cad3907646ac5a3a"><span class="id" title="notation">.-2</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="aperm_faithful"><span class="id" title="lemma">aperm_faithful</span></a> (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">faithful</span></a> <a class="idref" href="mathcomp.solvable.alt.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="aperm_faithful"><span class="id" title="lemma">aperm_faithful</span></a> (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">faithful</span></a> <a class="idref" href="mathcomp.solvable.alt.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef"><span class="id" title="section">SymAltDef</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">&quot;</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/>
+<span class="id" title="keyword">Notation</span> <a name="5639f842b98f65df33b56e1d8d4a2946"><span class="id" title="notation">&quot;</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">T</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Sym_' T") : <span class="id" title="var">group_scope</span>.<br/>
-<span class="id" title="keyword">Notation</span> <a name="0af815391ca483d74a2e8bf97e897bcd"><span class="id" title="notation">&quot;</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym_group"><span class="id" title="definition">Sym_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="fc8e40fe0cb216ea2f594c2c63586038"><span class="id" title="notation">&quot;</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym_group"><span class="id" title="definition">Sym_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">&quot;</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/>
+<span class="id" title="keyword">Notation</span> <a name="c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">&quot;</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">T</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Alt_' T") : <span class="id" title="var">group_scope</span>.<br/>
-<span class="id" title="keyword">Notation</span> <a name="692a66efc3505aab1e6d19a56b8b0139"><span class="id" title="notation">&quot;</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt_group"><span class="id" title="definition">Alt_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="988d46c711db28d95b743bfa12c213c4"><span class="id" title="notation">&quot;</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt_group"><span class="id" title="definition">Alt_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="trivial_Alt_2"><span class="id" title="lemma">trivial_Alt_2</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 2 <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.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</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/>
+<span class="id" title="keyword">Lemma</span> <a name="trivial_Alt_2"><span class="id" title="lemma">trivial_Alt_2</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="simple_Alt_3"><span class="id" title="lemma">simple_Alt_3</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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> 3 <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.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="simple_Alt_3"><span class="id" title="lemma">simple_Alt_3</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="not_simple_Alt_4"><span class="id" title="lemma">not_simple_Alt_4</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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> 4 <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.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="not_simple_Alt_4"><span class="id" title="lemma">not_simple_Alt_4</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 4 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5_base"><span class="id" title="lemma">simple_Alt5_base</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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> 5 <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.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5_base"><span class="id" title="lemma">simple_Alt5_base</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 5 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Section</span> <a name="Restrict"><span class="id" title="section">Restrict</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Variables</span> (<a name="Restrict.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Restrict.x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a>).<br/>
-<span class="id" title="keyword">Notation</span> <a name="T'"><span class="id" title="abbreviation">T'</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="T'"><span class="id" title="abbreviation">T'</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">{</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a>) :<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">p1</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.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</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.solvable.alt.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">else</span></a> 1 <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.alt.html#p1"><span class="id" title="variable">p1</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a>) :<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">p1</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> 1 <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.alt.html#p1"><span class="id" title="variable">p1</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <span class="id" title="var">p</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Sub"><span class="id" title="projection">Sub</span></a> ((<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.solvable.alt.html#rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <span class="id" title="var">p</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">fun</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Sub"><span class="id" title="projection">Sub</span></a> ((<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.solvable.alt.html#rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rfdP"><span class="id" title="lemma">rfdP</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rfdP"><span class="id" title="lemma">rfdP</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="rfd"><span class="id" title="definition">rfd</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="mathcomp.solvable.alt.html#rfdP"><span class="id" title="lemma">rfdP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Hypothesis</span> <a name="Restrict.card_T"><span class="id" title="variable">card_T</span></a> : 2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="Restrict.card_T"><span class="id" title="variable">card_T</span></a> : 2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rfd_morph"><span class="id" title="lemma">rfd_morph</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&amp;,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.alt.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rfd_morph"><span class="id" title="lemma">rfd_morph</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#5639f842b98f65df33b56e1d8d4a2946"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#5639f842b98f65df33b56e1d8d4a2946"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&amp;,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.alt.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rfd_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd_morph"><span class="id" title="lemma">rfd_morph</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="rgd_fun"><span class="id" title="definition">rgd_fun</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) :=<br/>
-&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x1</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> <a class="idref" href="mathcomp.solvable.alt.html#x1"><span class="id" title="variable">x1</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">u</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#sval"><span class="id" title="abbreviation">sval</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="var">u</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="rgd_fun"><span class="id" title="definition">rgd_fun</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">⇒</span></a> <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> <a class="idref" href="mathcomp.solvable.alt.html#x1"><span class="id" title="variable">x1</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">u</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#sval"><span class="id" title="abbreviation">sval</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="var">u</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rgdP"><span class="id" title="lemma">rgdP</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#rgd_fun"><span class="id" title="definition">rgd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rgdP"><span class="id" title="lemma">rgdP</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#rgd_fun"><span class="id" title="definition">rgd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="rgd"><span class="id" title="definition">rgd</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="mathcomp.solvable.alt.html#rgdP"><span class="id" title="lemma">rgdP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rfd_odd"><span class="id" title="lemma">rfd_odd</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.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.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="mathcomp.solvable.alt.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <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>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rfd_odd"><span class="id" title="lemma">rfd_odd</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="rfd_iso"><span class="id" title="lemma">rfd_iso</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T'</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rfd_iso"><span class="id" title="lemma">rfd_iso</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T'</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.alt.html#Restrict"><span class="id" title="section">Restrict</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5"><span class="id" title="lemma">simple_Alt5</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#08fe8636f4b45ae6787c490d19de1366"><span class="id" title="notation">≥</span></a> 5 <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.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5"><span class="id" title="lemma">simple_Alt5</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#73030c22bc0b1fa771c65aa5414c65f9"><span class="id" title="notation">≥</span></a> 5 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a>.<br/>
 </div>
 </div>
author	Enrico Tassi	2019-05-22 13:43:08 +0200
committer	Enrico Tassi	2019-05-22 15:34:14 +0200
commit	748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree	fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.solvable.alt.html
parent	415be3b908daadabf178a292c885db78e5b2c9a4 (diff)