generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.fingroup.perm.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 457 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.perm.html b/docs/htmldoc/mathcomp.fingroup.perm.html
new file mode 100644
index 0000000..e957ec7
--- /dev/null
+++ b/docs/htmldoc/mathcomp.fingroup.perm.html
@@ -0,0 +1,457 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>mathcomp.fingroup.perm</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.fingroup.perm</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This file contains the definition and properties associated to the group   
+ of permutations of an arbitrary finite type.                               
+     {perm T} == the type of permutations of a finite type T, i.e.,         
+                 injective (finite) functions from T to T. Permutations     
+                 coerce to CiC functions.                                   
+         'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1}  
+  perm_on A u == u is a permutation with support A, i.e., u only displaces  
+                 elements of A (u x != x implies x \in A).                  
+    tperm x y == the transposition of x, y.                                 
+    aperm x s == the image of x under the action of the permutation s.      
+              := s x                                                        
+   pcycle s x == the set of all elements that are in the same cycle of the  
+                 permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}.       
+    pcycles s == the set of all the cycles of the permutation s.            
+   (s : bool) == s is an odd permutation (the coercion is called odd_perm). 
+      dpair u == u is a pair (x, y) of distinct objects (i.e., x != y).     
+ lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over    
+                 (i |-&gt; j), that maps i to j and lift i k to lift j (s k).  
+ Canonical structures are defined allowing permutations to be an eqType,    
+ choiceType, countType, finType, subType, finGroupType; permutations with   
+ composition form a group, therefore inherit all generic group notations:   
+ 1 == identity permutation, * == composition, ^-1 == inverse permutation.    
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PermDefSection"><span class="id" title="section">PermDefSection</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="PermDefSection.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Inductive</span> <a name="perm_type"><span class="id" title="inductive">perm_type</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> :=<br/>
+&nbsp;&nbsp;<a name="Perm"><span class="id" title="constructor">Perm</span></a> (<span class="id" title="var">pval</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.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.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>) &amp; <a class="idref" href="mathcomp.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="variable">pval</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="pval"><span class="id" title="definition">pval</span></a> <span class="id" title="var">p</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.perm.html#Perm"><span class="id" title="constructor">Perm</span></a> <span class="id" title="var">f</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.fingroup.perm.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">f</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_of"><span class="id" title="definition">perm_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a>.<br/>
+<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_of_perm</span> : <span class="id" title="var">perm_of</span> &gt;-&gt; <span class="id" title="var">perm_type</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="pT"><span class="id" title="abbreviation">pT</span></a> := (<a class="idref" href="mathcomp.fingroup.perm.html#perm_of"><span class="id" title="definition">perm_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="definition">pval</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_eqMixin"><span class="id" title="definition">perm_eqMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_eqMixin"><span class="id" title="definition">perm_eqMixin</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_choiceMixin"><span class="id" title="definition">perm_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_choiceMixin"><span class="id" title="definition">perm_choiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_countMixin"><span class="id" title="definition">perm_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_countMixin"><span class="id" title="definition">perm_countMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subCountType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_finMixin"><span class="id" title="definition">perm_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_finMixin"><span class="id" title="definition">perm_finMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subCountType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_proof"><span class="id" title="lemma">perm_proof</span></a> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.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.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</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.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection"><span class="id" title="section">PermDefSection</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">&quot;</span></a>{ 'perm' T }" := (<a class="idref" href="mathcomp.fingroup.perm.html#perm_of"><span class="id" title="definition">perm_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'perm'  T }") : <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="ea6fcc91866185ddfad466ada7c10b27"><span class="id" title="notation">&quot;</span></a>''S_' n" := <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''S_' n").<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/>
+<span class="id" title="keyword">Parameter</span> <a name="PermDefSig.fun_of_perm"><span class="id" title="axiom">fun_of_perm</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">T</span>, <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.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.fingroup.perm.html#T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Parameter</span> <a name="PermDefSig.perm"><span class="id" title="axiom">perm</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.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.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Axiom</span> <a name="PermDefSig.fun_of_permE"><span class="id" title="axiom">fun_of_permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig.fun_of_perm"><span class="id" title="axiom">fun_of_perm</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.fingroup.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>.<br/>
+<span class="id" title="keyword">Axiom</span> <a name="PermDefSig.permE"><span class="id" title="axiom">permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig.perm"><span class="id" title="axiom">perm</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.fingroup.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="PermDef"><span class="id" title="module">PermDef</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="PermDef.fun_of_perm"><span class="id" title="definition">fun_of_perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="PermDef.perm"><span class="id" title="definition">perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="PermDef.fun_of_permE"><span class="id" title="lemma">fun_of_permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDef.fun_of_perm"><span class="id" title="definition">fun_of_perm</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.fingroup.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="PermDef.permE"><span class="id" title="lemma">permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDef.perm"><span class="id" title="definition">perm</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.fingroup.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>.  <br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDef"><span class="id" title="module">PermDef</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="fun_of_perm"><span class="id" title="abbreviation">fun_of_perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">PermDef.fun_of_perm</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">&quot;</span></a>@ 'perm'" := (@<a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="axiom">PermDef.perm</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 10, <span class="id" title="var">format</span> "@ 'perm'").<br/>
+<span class="id" title="keyword">Notation</span> <a name="perm"><span class="id" title="abbreviation">perm</span></a> := (@<a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="axiom">PermDef.perm</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fun_of_perm_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_permE"><span class="id" title="axiom">PermDef.fun_of_permE</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#permE"><span class="id" title="axiom">PermDef.permE</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">fun_of_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">Funclass</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Theory"><span class="id" title="section">Theory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="Theory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">S</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.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permP"><span class="id" title="lemma">permP</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pvalE"><span class="id" title="lemma">pvalE</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="definition">pval</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#Theory.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.fingroup.perm.html#Theory.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permE"><span class="id" title="lemma">permE</span></a> <span class="id" title="var">f</span> <span class="id" title="var">f_inj</span> : <a class="idref" href="mathcomp.fingroup.perm.html#ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">@</span></a><a class="idref" href="mathcomp.fingroup.perm.html#ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">T</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ed3415d539756427d396dbdd3cf8051f"><span class="id" title="notation">f_inj</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_inj"><span class="id" title="lemma">perm_inj</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">perm_inj</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_onto"><span class="id" title="lemma">perm_onto</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predT"><span class="id" title="definition">predT</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_one"><span class="id" title="definition">perm_one</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#inj_id"><span class="id" title="lemma">inj_id</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_invK"><span class="id" title="lemma">perm_invK</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.fintype.html#iinv"><span class="id" title="definition">iinv</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_onto"><span class="id" title="lemma">perm_onto</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_inv"><span class="id" title="definition">perm_inv</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_invK"><span class="id" title="lemma">perm_invK</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_mul"><span class="id" title="definition">perm_mul</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#inj_comp"><span class="id" title="lemma">inj_comp</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_inj"><span class="id" title="lemma">perm_inj</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#perm_inj"><span class="id" title="lemma">perm_inj</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_oneP"><span class="id" title="lemma">perm_oneP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_one"><span class="id" title="definition">perm_one</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_invP"><span class="id" title="lemma">perm_invP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_one"><span class="id" title="definition">perm_one</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_inv"><span class="id" title="definition">perm_inv</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_mulP"><span class="id" title="lemma">perm_mulP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_of_baseFinGroupMixin"><span class="id" title="definition">perm_of_baseFinGroupMixin</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.mixin_of"><span class="id" title="record">FinGroup.mixin_of</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin"><span class="id" title="definition">FinGroup.Mixin</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mulP"><span class="id" title="lemma">perm_mulP</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_oneP"><span class="id" title="lemma">perm_oneP</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_invP"><span class="id" title="lemma">perm_invP</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_baseFinGroupType</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.BaseFinGroupType"><span class="id" title="abbreviation">BaseFinGroupType</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#perm_of_baseFinGroupMixin"><span class="id" title="definition">perm_of_baseFinGroupMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_finGroupType</span> := @<a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType"><span class="id" title="abbreviation">FinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_baseFinGroupType"><span class="id" title="definition">perm_baseFinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_invP"><span class="id" title="lemma">perm_invP</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_of_baseFinGroupType</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_of_finGroupType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm1"><span class="id" title="lemma">perm1</span></a> <span class="id" title="var">x</span> : (1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permM"><span class="id" title="lemma">permM</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permK"><span class="id" title="lemma">permK</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permKV"><span class="id" title="lemma">permKV</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permJ"><span class="id" title="lemma">permJ</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="permX"><span class="id" title="lemma">permX</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="im_permV"><span class="id" title="lemma">im_permV</span></a> <span class="id" title="var">s</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#aa0c936d7feb8f26825e601735c0125f"><span class="id" title="notation">@^-1:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="preim_permV"><span class="id" title="lemma">preim_permV</span></a> <span class="id" title="var">s</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#aa0c936d7feb8f26825e601735c0125f"><span class="id" title="notation">@^-1:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="perm_on"><span class="id" title="definition">perm_on</span></a> <span class="id" title="var">S</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">s</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</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.perm.html#S"><span class="id" title="variable">S</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_closed"><span class="id" title="lemma">perm_closed</span></a> <span class="id" title="var">S</span> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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="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.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_on1"><span class="id" title="lemma">perm_on1</span></a> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> 1.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_onM"><span class="id" title="lemma">perm_onM</span></a> <span class="id" title="var">H</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="out_perm"><span class="id" title="lemma">out_perm</span></a> <span class="id" title="var">S</span> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#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.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="im_perm_on"><span class="id" title="lemma">im_perm_on</span></a> <span class="id" title="var">u</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tperm_proof"><span class="id" title="lemma">tperm_proof</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">fun</span></a> <span class="id" title="var">z</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#208083cddfca3726231c4e84b7c928c1"><span class="id" title="notation">|-&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#208083cddfca3726231c4e84b7c928c1"><span class="id" title="notation">|-&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#98daeff9b38ed89b3ac0db77b4ceb901"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tperm"><span class="id" title="definition">tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm_proof"><span class="id" title="lemma">tperm_proof</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#Theory.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> <span class="id" title="keyword">Type</span> :=<br/>
+&nbsp;&nbsp;| <a name="TpermFirst"><span class="id" title="constructor">TpermFirst</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>          : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><br/>
+&nbsp;&nbsp;| <a name="TpermSecond"><span class="id" title="constructor">TpermSecond</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>         : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><br/>
+&nbsp;&nbsp;| <a name="TpermNone"><span class="id" title="constructor">TpermNone</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> &amp; <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermP"><span class="id" title="lemma">tpermP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermL"><span class="id" title="lemma">tpermL</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermR"><span class="id" title="lemma">tpermR</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermD"><span class="id" title="lemma">tpermD</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermC"><span class="id" title="lemma">tpermC</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tperm1"><span class="id" title="lemma">tperm1</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermK"><span class="id" title="lemma">tpermK</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermKg"><span class="id" title="lemma">tpermKg</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#mulg"><span class="id" title="definition">mulg</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>)).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermV"><span class="id" title="lemma">tpermV</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">)^-1</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.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tperm2"><span class="id" title="lemma">tperm2</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_perm"><span class="id" title="lemma">card_perm</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#A"><span class="id" title="variable">A</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.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><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.fingroup.perm.html#A"><span class="id" title="variable">A</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#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#Theory"><span class="id" title="section">Theory</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="inj_tperm"><span class="id" title="lemma">inj_tperm</span></a> (<span class="id" title="var">T</span> <span class="id" title="var">T'</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#T'"><span class="id" title="variable">T'</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/>
+&nbsp;&nbsp;<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.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tpermJ"><span class="id" title="lemma">tpermJ</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tuple_perm_eqP"><span class="id" title="lemma">tuple_perm_eqP</span></a> {<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>} {<span class="id" title="var">n</span>} {<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#T"><span class="id" title="variable">T</span></a>} {<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#T"><span class="id" title="variable">T</span></a>} :<br/>
+&nbsp;&nbsp;<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.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#ea6fcc91866185ddfad466ada7c10b27"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#ea6fcc91866185ddfad466ada7c10b27"><span class="id" title="notation">S_n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">|</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#perm_eq"><span class="id" title="definition">perm_eq</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="PermutationParity"><span class="id" title="section">PermutationParity</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="PermutationParity.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Note that pcycle s x is the orbit of x by &lt; [s]&gt; under the action aperm. 
+ Hence, the pcycle lemmas below are special cases of more general lemmas 
+ on orbits that will be stated in action.v.                              
+   Defining pcycle directly here avoids a dependency of matrix.v on      
+ action.v and hence morphism.v.                                           
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="aperm"><span class="id" title="definition">aperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="pcycle"><span class="id" title="definition">pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.fingroup.perm.html#aperm"><span class="id" title="definition">aperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="pcycles"><span class="id" title="definition">pcycles</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="odd_perm"><span class="id" title="definition">odd_perm</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.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.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="apermE"><span class="id" title="lemma">apermE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#aperm"><span class="id" title="definition">aperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_pcycle"><span class="id" title="lemma">mem_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">i</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pcycle_id"><span class="id" title="lemma">pcycle_id</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="uniq_traject_pcycle"><span class="id" title="lemma">uniq_traject_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pcycle_traject"><span class="id" title="lemma">pcycle_traject</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="iter_pcycle"><span class="id" title="lemma">iter_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_pcycle_mem"><span class="id" title="lemma">eq_pcycle_mem</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pcycle_sym"><span class="id" title="lemma">pcycle_sym</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pcycle_perm"><span class="id" title="lemma">pcycle_perm</span></a> <span class="id" title="var">s</span> <span class="id" title="var">i</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> ((<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ncycles_mul_tperm"><span class="id" title="lemma">ncycles_mul_tperm</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="keyword">let</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">).*2</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.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_perm1"><span class="id" title="lemma">odd_perm1</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_mul_tperm"><span class="id" title="lemma">odd_mul_tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_tperm"><span class="id" title="lemma">odd_tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="dpair"><span class="id" title="definition">dpair</span></a> (<span class="id" title="var">eT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">t</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#eT"><span class="id" title="variable">eT</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prod_tpermP"><span class="id" title="lemma">prod_tpermP</span></a> <span class="id" title="var">s</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">ts</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">(</span></a><span class="id" title="var">t</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#dpair"><span class="id" title="definition">dpair</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_perm_prod"><span class="id" title="lemma">odd_perm_prod</span></a> <span class="id" title="var">ts</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#dpair"><span class="id" title="definition">dpair</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">(</span></a><span class="id" title="var">t</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#644e2d6a4fd9b4978c70acde75bf082b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_permM"><span class="id" title="lemma">odd_permM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s2"><span class="id" title="variable">s2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_permV"><span class="id" title="lemma">odd_permV</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</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.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_permJ"><span class="id" title="lemma">odd_permJ</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity"><span class="id" title="section">PermutationParity</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">bool</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="LiftPerm"><span class="id" title="section">LiftPerm</span></a>.<br/>
+</div>
+
+<div class="doc">
+ Somewhat more specialised constructs for permutations on ordinals.  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="LiftPerm.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">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#ea6fcc91866185ddfad466ada7c10b27"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#ea6fcc91866185ddfad466ada7c10b27"><span class="id" title="notation">S_n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> <span class="id" title="var">k</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#unlift"><span class="id" title="definition">unlift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">k'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="var">k'</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_permK"><span class="id" title="lemma">lift_permK</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="lift_perm"><span class="id" title="definition">lift_perm</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#lift_permK"><span class="id" title="lemma">lift_permK</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_perm_id"><span class="id" title="lemma">lift_perm_id</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</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.fingroup.perm.html#j"><span class="id" title="variable">j</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_perm_lift"><span class="id" title="lemma">lift_perm_lift</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> <span class="id" title="var">k'</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k'"><span class="id" title="variable">k'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k'"><span class="id" title="variable">k'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_permM"><span class="id" title="lemma">lift_permM</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">k</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_perm1"><span class="id" title="lemma">lift_perm1</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="lift_permV"><span class="id" title="lemma">lift_permV</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">)^-1</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.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="odd_lift_perm"><span class="id" title="lemma">odd_lift_perm</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#LiftPerm"><span class="id" title="section">LiftPerm</span></a>.<br/>
+
+<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
+\ No newline at end of file
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.fingroup.perm.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)