diff options
| 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.primitive_action.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.primitive_action.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.primitive_action.html | 89 |
1 files changed, 43 insertions, 46 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.primitive_action.html b/docs/htmldoc/mathcomp.solvable.primitive_action.html index ee8d1dc..fcf9d4a 100644 --- a/docs/htmldoc/mathcomp.solvable.primitive_action.html +++ b/docs/htmldoc/mathcomp.solvable.primitive_action.html @@ -21,7 +21,6 @@ <div class="code"> <span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> Distributed under the terms of CeCILL-B. *)</span><br/> -<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> <br/> </div> @@ -54,15 +53,15 @@ <br/> <span class="id" title="keyword">Variables</span> (<a name="PrimitiveDef.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="PrimitiveDef.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="PrimitiveDef.A"><span class="id" title="variable">A</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.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="PrimitiveDef.A"><span class="id" title="variable">A</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.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>).<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="imprimitivity_system"><span class="id" title="definition">imprimitivity_system</span></a> <span class="id" title="var">Q</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#partition"><span class="id" title="definition">partition</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#495b9dab41eed2da7a7d91b1cb8498af"><span class="id" title="notation">^*</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">&</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#432e31800fc09abd260feb634dbbd1af"><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.primitive_action.html#Q"><span class="id" title="variable">Q</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#432e31800fc09abd260feb634dbbd1af"><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.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</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.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">]</span></a>.<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#partition"><span class="id" title="definition">partition</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#1ebbed7bbef8371b25df9685ff0f4361"><span class="id" title="notation">^*</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cf4676be165a6295cd8b63fc45b45d8a"><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.primitive_action.html#Q"><span class="id" title="variable">Q</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#cf4676be165a6295cd8b63fc45b45d8a"><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.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</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.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="primitive"><span class="id" title="definition">primitive</span></a> :=<br/> - <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="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.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">∃</span></a> <span class="id" title="var">Q</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#imprimitivity_system"><span class="id" title="definition">imprimitivity_system</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">]</span></a>.<br/> + <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">∃</span></a> <span class="id" title="var">Q</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#imprimitivity_system"><span class="id" title="definition">imprimitivity_system</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef"><span class="id" title="section">PrimitiveDef</span></a>.<br/> @@ -70,27 +69,25 @@ <br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">"</span></a>[ 'primitive' A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#primitive"><span class="id" title="definition">primitive</span></a> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">"</span></a>[ 'primitive' A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#primitive"><span class="id" title="definition">primitive</span></a> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'primitive' A , 'on' S | to ]") : <span class="id" title="var">form_scope</span>.<br/> <br/> - -<br/> <span class="id" title="keyword">Section</span> <a name="Primitive"><span class="id" title="section">Primitive</span></a>.<br/> <br/> <span class="id" title="keyword">Variables</span> (<a name="Primitive.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="Primitive.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="Primitive.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="Primitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>) (<a name="Primitive.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="Primitive.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="Primitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="Primitive.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>).<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="trans_prim_astab"><span class="id" title="lemma">trans_prim_astab</span></a> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#Primitive.S"><span class="id" title="variable">S</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.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a>.<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#Primitive.S"><span class="id" title="variable">S</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.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="prim_trans_norm"><span class="id" title="lemma">prim_trans_norm</span></a> (<span class="id" title="var">H</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.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</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.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="prim_trans_norm"><span class="id" title="lemma">prim_trans_norm</span></a> (<span class="id" title="var">H</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.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</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.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive"><span class="id" title="section">Primitive</span></a>.<br/> @@ -100,10 +97,10 @@ <br/> <span class="id" title="keyword">Variables</span> (<a name="NactionDef.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NactionDef.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NactionDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>) (<a name="NactionDef.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="NactionDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NactionDef.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="n_act"><span class="id" title="definition">n_act</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="n_act"><span class="id" title="definition">n_act</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">Fact</span> <a name="n_act_is_action"><span class="id" title="lemma">n_act_is_action</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_action"><span class="id" title="definition">is_action</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#n_act"><span class="id" title="definition">n_act</span></a>.<br/> @@ -115,26 +112,26 @@ <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef"><span class="id" title="section">NactionDef</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="a34aaddd6f4c8073b4fe8bc7ff30e5ca"><span class="id" title="notation">"</span></a>to * n" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#n_act_action"><span class="id" title="definition">n_act_action</span></a> <span class="id" title="var">to</span> <span class="id" title="var">n</span>) : <span class="id" title="var">action_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="7472b0b72b7b3e0244b040606fd1fa69"><span class="id" title="notation">"</span></a>to * n" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#n_act_action"><span class="id" title="definition">n_act_action</span></a> <span class="id" title="var">to</span> <span class="id" title="var">n</span>) : <span class="id" title="var">action_scope</span>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="NTransitive"><span class="id" title="section">NTransitive</span></a>.<br/> <br/> <span class="id" title="keyword">Variables</span> (<a name="NTransitive.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitive.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitive.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="NTransitive.A"><span class="id" title="variable">A</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.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="NTransitive.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="NTransitive.A"><span class="id" title="variable">A</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.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="dtuple_on"><span class="id" title="definition">dtuple_on</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">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.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="ntransitive"><span class="id" title="definition">ntransitive</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a34aaddd6f4c8073b4fe8bc7ff30e5ca"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="dtuple_on"><span class="id" title="definition">dtuple_on</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">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.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="ntransitive"><span class="id" title="definition">ntransitive</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#7472b0b72b7b3e0244b040606fd1fa69"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="dtuple_onP"><span class="id" title="lemma">dtuple_onP</span></a> <span class="id" title="var">t</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<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.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.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.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a>) (<a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>).<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<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.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#i"><span class="id" title="variable">i</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.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a>) (<a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>).<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="n_act_dtuple"><span class="id" title="lemma">n_act_dtuple</span></a> <span class="id" title="var">t</span> <span class="id" title="var">a</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</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.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</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.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>.<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</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.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</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.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</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.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive"><span class="id" title="section">NTransitive</span></a>.<br/> @@ -142,11 +139,11 @@ <br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">"</span></a>n .-dtuple ( S )" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <span class="id" title="var">n</span> <span class="id" title="var">S</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="9437d70414518cee40513da45e8f965b"><span class="id" title="notation">"</span></a>n .-dtuple ( S )" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <span class="id" title="var">n</span> <span class="id" title="var">S</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "n .-dtuple ( S )") : <span class="id" title="var">set_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">"</span></a>[ 'transitive' ^ n A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#ntransitive"><span class="id" title="definition">ntransitive</span></a> <span class="id" title="var">n</span> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">"</span></a>[ 'transitive' ^ n A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#ntransitive"><span class="id" title="definition">ntransitive</span></a> <span class="id" title="var">n</span> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8,<br/> <span class="id" title="var">format</span> "[ 'transitive' ^ n A , 'on' S | to ]") : <span class="id" title="var">form_scope</span>.<br/> @@ -155,46 +152,46 @@ <br/> <span class="id" title="keyword">Variables</span> (<a name="NTransitveProp.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitveProp.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitveProp.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="NTransitveProp.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_uniq_tuple"><span class="id" title="lemma">card_uniq_tuple</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.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> <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_uniq_tuple"><span class="id" title="lemma">card_uniq_tuple</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.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> <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="n_act0"><span class="id" title="lemma">n_act0</span></a> (<span class="id" title="var">t</span> : 0<a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="n_act0"><span class="id" title="lemma">n_act0</span></a> (<span class="id" title="var">t</span> : 0<a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add"><span class="id" title="lemma">dtuple_on_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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">\</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add"><span class="id" title="lemma">dtuple_on_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><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">\</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add_D1"><span class="id" title="lemma">dtuple_on_add_D1</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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">\</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a><br/> - <a class="idref" href="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.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67a75c8b7ac489919adc46e74581b83e"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add_D1"><span class="id" title="lemma">dtuple_on_add_D1</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><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">\</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><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><br/> + <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.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_subset"><span class="id" title="lemma">dtuple_on_subset</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">S1</span> <span class="id" title="var">S2</span> : <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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">t</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</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.primitive_action.html#S2"><span class="id" title="variable">S2</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.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S2"><span class="id" title="variable">S2</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_subset"><span class="id" title="lemma">dtuple_on_subset</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">S1</span> <span class="id" title="var">S2</span> : <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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">t</span> :<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</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.primitive_action.html#S2"><span class="id" title="variable">S2</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.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S2"><span class="id" title="variable">S2</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="n_act_add"><span class="id" title="lemma">n_act_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="n_act_add"><span class="id" title="lemma">n_act_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> :<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="ntransitive0"><span class="id" title="lemma">ntransitive0</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>0 <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</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="ntransitive0"><span class="id" title="lemma">ntransitive0</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>0 <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</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="ntransitive_weak"><span class="id" title="lemma">ntransitive_weak</span></a> <span class="id" title="var">k</span> <span class="id" title="var">m</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <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.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</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="ntransitive1"><span class="id" title="lemma">ntransitive1</span></a> <span class="id" title="var">m</span> :<br/> - 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a>.<br/> + 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="ntransitive_primitive"><span class="id" title="lemma">ntransitive_primitive</span></a> <span class="id" title="var">m</span> :<br/> - 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">]</span></a>.<br/> + 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</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#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp"><span class="id" title="section">NTransitveProp</span></a>.<br/> @@ -204,7 +201,7 @@ <br/> <span class="id" title="keyword">Variables</span> (<a name="NTransitveProp1.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitveProp1.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitveProp1.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="NTransitveProp1.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.G"><span class="id" title="variable">G</span></a> : <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.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.S"><span class="id" title="variable">S</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.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>).<br/> <br/> </div> @@ -214,8 +211,8 @@ </div> <div class="code"> <span class="id" title="keyword">Theorem</span> <a name="stab_ntransitive"><span class="id" title="lemma">stab_ntransitive</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> :<br/> - 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67a75c8b7ac489919adc46e74581b83e"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/> + 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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.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.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/> <br/> </div> @@ -225,9 +222,9 @@ </div> <div class="code"> <span class="id" title="keyword">Theorem</span> <a name="stab_ntransitiveI"><span class="id" title="lemma">stab_ntransitiveI</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67a75c8b7ac489919adc46e74581b83e"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <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.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</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#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <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.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</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.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</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#NTransitveProp1.to"><span class="id" title="variable">to</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">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1"><span class="id" title="section">NTransitveProp1</span></a>.<br/> |