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.ssreflect.path.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 761 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.path.html b/docs/htmldoc/mathcomp.ssreflect.path.html
new file mode 100644
index 0000000..27e0fdf
--- /dev/null
+++ b/docs/htmldoc/mathcomp.ssreflect.path.html
@@ -0,0 +1,761 @@
+<!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.ssreflect.path</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.ssreflect.path</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">
+    The basic theory of paths over an eqType; this file is essentially a    
+ complement to seq.v. Paths are non-empty sequences that obey a progression 
+ relation. They are passed around in three parts: the head and tail of the  
+ sequence, and a proof of (boolean) predicate asserting the progression.    
+ This "exploded" view is rarely embarrassing, as the first two parameters   
+ are usually inferred from the type of the third; on the contrary, it saves 
+ the hassle of constantly constructing and destructing a dependent record.  
+    We define similarly cycles, for which we allow the empty sequence,      
+ which represents a non-rooted empty cycle; by contrast, the "empty" path   
+ from a point x is the one-item sequence containing only x.                 
+   We allow duplicates; uniqueness, if desired (as is the case for several  
+ geometric constructions), must be asserted separately. We do provide       
+ shorthand, but only for cycles, because the equational properties of       
+ "path" and "uniq" are unfortunately  incompatible (esp. wrt "cat").        
+    We define notations for the common cases of function paths, where the   
+ progress relation is actually a function. In detail:                       
+   path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we     
+                 e x_i x{i+1} for all i &lt; n. The path x :: p starts at x   
+                 and ends at last x p.                                      
+  fpath f x p == x :: p is an f-path, where f is a function, i.e., p is of  
+                 the form [:: f x; f (f x); ... ]. This is just a notation   
+                 for path (frel f) x p.                                     
+   sorted e s == s is an e-sorted sequence: either s = [:: ], or s = x :: p  
+                 is an e-path (this is oten used with e = leq or ltn).      
+    cycle e c == c is an e-cycle: either c = [:: ], or c = x :: p with       
+                 x :: (rcons p x) an e-path.                                
+   fcycle f c == c is an f-cycle, for a function f.                         
+ traject f x n == the f-path of size n starting at x                        
+              := [:: x; f x; ...; iter n.-1 f x]                            
+ looping f x n == the f-paths of size greater than n starting at x loop     
+                 back, or, equivalently, traject f x n contains all         
+                 iterates of f at x.                                        
+ merge e s1 s2 == the e-sorted merge of sequences s1 and s2: this is always 
+                 a permutation of s1 ++ s2, and is e-sorted when s1 and s2  
+                 are and e is total.                                        
+     sort e s == a permutation of the sequence s, that is e-sorted when e   
+                 is total (computed by a merge sort with the merge function 
+                 above).                                                    
+   mem2 s x y == x, then y occur in the sequence (path) s; this is          
+                 non-strict: mem2 s x x = (x \in s).                        
+     next c x == the successor of the first occurrence of x in the sequence 
+                 c (viewed as a cycle), or x if x \notin c.                 
+     prev c x == the predecessor of the first occurrence of x in the        
+                 sequence c (viewed as a cycle), or x if x \notin c.        
+    arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting  
+                 at the first occurrence of x in c, and ending just before  
+                 the next ocurrence of y (in cycle order); arc c x y        
+                 returns an unspecified sub-arc of c if x and y do not both 
+                 occur in c.                                                
+  ucycle e c &lt;-&gt; ucycleb e c (ucycle e c is a Coercion target of type Prop) 
+ ufcycle f c &lt;-&gt; c is a simple f-cycle, for a function f.                   
+  shorten x p == the tail a duplicate-free subpath of x :: p with the same  
+                 endpoints (x and last x p), obtained by removing all loops 
+                 from x :: p.                                               
+ rel_base e e' h b &lt;-&gt; the function h is a functor from relation e to       
+                 relation e', EXCEPT at points whose image under h satisfy  
+                 the "base" predicate b:                                    
+                    e' (h x) (h y) = e x y UNLESS b (h x) holds             
+                 This is the statement of the side condition of the path    
+                 functorial mapping lemma map_path.                         
+ fun_base f f' h b &lt;-&gt; the function h is a functor from function f to f',   
+                 except at the preimage of predicate b under h.             
+ We also provide three segmenting dependently-typed lemmas (splitP, splitPl 
+ and splitPr) whose elimination split a path x0 :: p at an internal point x 
+ as follows:                                                                
+<ul class="doclist">
+<li> splitP applies when x \in p; it replaces p with (rcons p1 x ++ p2), so  
+    that x appears explicitly at the end of the left part. The elimination  
+    of splitP will also simultaneously replace take (index x p) with p1 and 
+    drop (index x p).+1 p with p2.                                          
+
+</li>
+<li> splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and     
+    simulaneously generates an equation x = last x0 p.                      
+
+</li>
+<li> splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x  
+    appears explicitly at the start of the right part.                      
+
+</li>
+</ul>
+ The parts p1 and p2 are computed using index/take/drop in all cases, but   
+ only splitP attemps to subsitute the explicit values. The substitution of  
+ p can be deferred using the dependent equation generation feature of       
+ ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p =&gt; [p1 p2] generates    
+ the equation p = p1 ++ p2 instead of performing the substitution outright. 
+   Similarly, eliminating the loop removal lemma shortenP simultaneously    
+ replaces shorten e x p with a fresh constant p', and last x p with         
+ last x p'.                                                                 
+   Note that although all "path" functions actually operate on the          
+ underlying sequence, we provide a series of lemmas that define their       
+ interaction with thepath and cycle predicates, e.g., the cat_path equation 
+ can be used to split the path predicate after splitting the underlying     
+ sequence.                                                                   
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Paths"><span class="id" title="section">Paths</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Paths.n0"><span class="id" title="variable">n0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="Paths.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Paths.Path"><span class="id" title="section">Path</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Paths.Path.x0_cycle"><span class="id" title="variable">x0_cycle</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#Paths.T"><span class="id" title="variable">T</span></a>) (<a name="Paths.Path.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="path"><span class="id" title="definition">path</span></a> <span class="id" title="var">x</span> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.Path.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <span class="id" title="var">y</span> <span class="id" title="var">p'</span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cat_path"><span class="id" title="lemma">cat_path</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</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.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rcons_path"><span class="id" title="lemma">rcons_path</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.Path.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pathP"><span class="id" title="lemma">pathP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> <span class="id" title="var">x0</span> :<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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.Path.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x0"><span class="id" title="variable">x0</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a>))<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="cycle"><span class="id" title="definition">cycle</span></a> <span class="id" title="var">p</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <span class="id" title="var">x</span> (<a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> <span class="id" title="var">p'</span> <span class="id" title="var">x</span>) <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cycle_path"><span class="id" title="lemma">cycle_path</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.Path.x0_cycle"><span class="id" title="variable">x0_cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rot_cycle"><span class="id" title="lemma">rot_cycle</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rotr_cycle"><span class="id" title="lemma">rotr_cycle</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rotr"><span class="id" title="definition">rotr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#Paths.Path"><span class="id" title="section">Path</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_path"><span class="id" title="lemma">eq_path</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</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.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_cycle"><span class="id" title="lemma">eq_cycle</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</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.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sub_path"><span class="id" title="lemma">sub_path</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#subrel"><span class="id" title="definition">subrel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</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">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">p</span>, <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rev_path"><span class="id" title="lemma">rev_path</span></a> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">p</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">z</span> ⇒ <a class="idref" href="mathcomp.ssreflect.path.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#z"><span class="id" title="variable">z</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#Paths"><span class="id" title="section">Paths</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="EqPath"><span class="id" title="section">EqPath</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="EqPath.n0"><span class="id" title="variable">n0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="EqPath.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a name="EqPath.x0_cycle"><span class="id" title="variable">x0_cycle</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="EqPath.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="split"><span class="id" title="inductive">split</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.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="Split"><span class="id" title="constructor">Split</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> : <a class="idref" href="mathcomp.ssreflect.path.html#split"><span class="id" title="inductive">split</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="splitP"><span class="id" title="lemma">splitP</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> (<span class="id" title="var">i</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#split"><span class="id" title="inductive">split</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#take"><span class="id" title="definition">take</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#drop"><span class="id" title="definition">drop</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="splitl"><span class="id" title="inductive">splitl</span></a> <span class="id" title="var">x1</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.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="Splitl"><span class="id" title="constructor">Splitl</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</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.path.html#x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#splitl"><span class="id" title="inductive">splitl</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="splitPl"><span class="id" title="lemma">splitPl</span></a> <span class="id" title="var">x1</span> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#splitl"><span class="id" title="inductive">splitl</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x1"><span class="id" title="variable">x1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="splitr"><span class="id" title="inductive">splitr</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.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="Splitr"><span class="id" title="constructor">Splitr</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> : <a class="idref" href="mathcomp.ssreflect.path.html#splitr"><span class="id" title="inductive">splitr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="splitPr"><span class="id" title="lemma">splitPr</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#splitr"><span class="id" title="inductive">splitr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="next_at"><span class="id" title="definition">next_at</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y0</span> <span class="id" title="var">y</span> <span class="id" title="var">p</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><br/>
+&nbsp;&nbsp;| <span class="id" title="var">y'</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <span class="id" title="var">y'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#next_at"><span class="id" title="definition">next_at</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y0"><span class="id" title="variable">y0</span></a> <span class="id" title="var">y'</span> <span class="id" title="var">p'</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="next"><span class="id" title="definition">next</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#next_at"><span class="id" title="definition">next_at</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="var">y</span> <span class="id" title="var">p'</span> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="prev_at"><span class="id" title="definition">prev_at</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y0</span> <span class="id" title="var">y</span> <span class="id" title="var">p</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>     ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><br/>
+&nbsp;&nbsp;| <span class="id" title="var">y'</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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> <span class="id" title="var">y'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#prev_at"><span class="id" title="definition">prev_at</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y0"><span class="id" title="variable">y0</span></a> <span class="id" title="var">y'</span> <span class="id" title="var">p'</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="prev"><span class="id" title="definition">prev</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#prev_at"><span class="id" title="definition">prev_at</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="var">y</span> <span class="id" title="var">p'</span> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_nth"><span class="id" title="lemma">next_nth</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <span class="id" title="var">y</span> <span class="id" title="var">p'</span> (<a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_nth"><span class="id" title="lemma">prev_nth</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">p'</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_next"><span class="id" title="lemma">mem_next</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</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.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_prev"><span class="id" title="lemma">mem_prev</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</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.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ ucycleb is the boolean predicate, but ucycle is defined as a Prop 
+ so that it can be used as a coercion target.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="ucycleb"><span class="id" title="definition">ucycleb</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <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#p"><span class="id" title="variable">p</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="ucycle"><span class="id" title="definition">ucycle</span></a> <span class="id" title="var">p</span> : <span class="id" title="keyword">Prop</span> := <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <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#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Projections, used for creating local lemmas.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="ucycle_cycle"><span class="id" title="lemma">ucycle_cycle</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ucycle_uniq"><span class="id" title="lemma">ucycle_uniq</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_cycle"><span class="id" title="lemma">next_cycle</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_cycle"><span class="id" title="lemma">prev_cycle</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rot_ucycle"><span class="id" title="lemma">rot_ucycle</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rotr_ucycle"><span class="id" title="lemma">rotr_ucycle</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rotr"><span class="id" title="definition">rotr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ The "appears no later" partial preorder defined by a path.  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="mem2"><span class="id" title="definition">mem2</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.seq.html#drop"><span class="id" title="definition">drop</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2l"><span class="id" title="lemma">mem2l</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2lf"><span class="id" title="lemma">mem2lf</span></a> {<span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>} : <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2r"><span class="id" title="lemma">mem2r</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2rf"><span class="id" title="lemma">mem2rf</span></a> {<span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>} : <a class="idref" href="mathcomp.ssreflect.path.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#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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_cat"><span class="id" title="lemma">mem2_cat</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_splice"><span class="id" title="lemma">mem2_splice</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p3</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">p2</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_splice1"><span class="id" title="lemma">mem2_splice1</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p3</span> <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="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_cons"><span class="id" title="lemma">mem2_cons</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.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="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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.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.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.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>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_seq1"><span class="id" title="lemma">mem2_seq1</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.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_last"><span class="id" title="lemma">mem2_last</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2l_cat"><span class="id" title="lemma">mem2l_cat</span></a> {<span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="var">x</span>} : <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p1"><span class="id" title="variable">p1</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.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) <a class="idref" href="mathcomp.ssreflect.path.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.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2r_cat"><span class="id" title="lemma">mem2r_cat</span></a> {<span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>} : <a class="idref" href="mathcomp.ssreflect.path.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#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.ssreflect.path.html#p2"><span class="id" title="variable">p2</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.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2lr_splice"><span class="id" title="lemma">mem2lr_splice</span></a> {<span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="var">p3</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>} :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p2"><span class="id" title="variable">p2</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.path.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#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.ssreflect.path.html#p2"><span class="id" title="variable">p2</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.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p3"><span class="id" title="variable">p3</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="split2r"><span class="id" title="inductive">split2r</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.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="Split2r"><span class="id" title="constructor">Split2r</span></a> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#split2r"><span class="id" title="inductive">split2r</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="splitP2r"><span class="id" title="lemma">splitP2r</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#split2r"><span class="id" title="inductive">split2r</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="shorten"><span class="id" title="definition">shorten</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#shorten"><span class="id" title="definition">shorten</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">p'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#shorten"><span class="id" title="definition">shorten</span></a> <span class="id" title="var">y</span> <span class="id" title="var">p'</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="shorten_spec"><span class="id" title="inductive">shorten_spec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.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;&nbsp;<a name="ShortenSpec"><span class="id" title="constructor">ShortenSpec</span></a> <span class="id" title="var">p'</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a> &amp; <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#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#subpred"><span class="id" title="definition">subpred</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#shorten_spec"><span class="id" title="inductive">shorten_spec</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="shortenP"><span class="id" title="lemma">shortenP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#shorten_spec"><span class="id" title="inductive">shorten_spec</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#shorten"><span class="id" title="definition">shorten</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#EqPath"><span class="id" title="section">EqPath</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Ordered paths and sorting.  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="SortSeq"><span class="id" title="section">SortSeq</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="SortSeq.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>.<br/>
+<span class="id" title="keyword">Variable</span> <a name="SortSeq.leT"><span class="id" title="variable">leT</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sorted"><span class="id" title="definition">sorted</span></a> <span class="id" title="var">s</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">s'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s'</span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="path_sorted"><span class="id" title="lemma">path_sorted</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="path_min_sorted"><span class="id" title="lemma">path_min_sorted</span></a> <span class="id" title="var">x</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.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.path.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Section</span> <a name="SortSeq.Transitive"><span class="id" title="section">Transitive</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="SortSeq.Transitive.leT_tr"><span class="id" title="variable">leT_tr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="subseq_order_path"><span class="id" title="lemma">subseq_order_path</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.seq.html#subseq"><span class="id" title="definition">subseq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="order_path_min"><span class="id" title="lemma">order_path_min</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="subseq_sorted"><span class="id" title="lemma">subseq_sorted</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#subseq"><span class="id" title="definition">subseq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sorted_filter"><span class="id" title="lemma">sorted_filter</span></a> <span class="id" title="var">a</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#filter"><span class="id" title="definition">filter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sorted_uniq"><span class="id" title="lemma">sorted_uniq</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#irreflexive"><span class="id" title="definition">irreflexive</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</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">∀</span> <span class="id" title="var">s</span>, <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_sorted"><span class="id" title="lemma">eq_sorted</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#antisymmetric"><span class="id" title="definition">antisymmetric</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span>, <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#perm_eq"><span class="id" title="definition">perm_eq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#s2"><span class="id" title="variable">s2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_sorted_irr"><span class="id" title="lemma">eq_sorted_irr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#irreflexive"><span class="id" title="definition">irreflexive</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span>, <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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#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#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#s2"><span class="id" title="variable">s2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.Transitive"><span class="id" title="section">Transitive</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="SortSeq.leT_total"><span class="id" title="variable">leT_total</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#total"><span class="id" title="definition">total</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="merge"><span class="id" title="definition">merge</span></a> <span class="id" title="var">s1</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">x1</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">s1'</span> <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="keyword">fix</span> <span class="id" title="var">merge_s1</span> <span class="id" title="var">s2</span> :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">x2</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">s2'</span> <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <span class="id" title="var">x2</span> <span class="id" title="var">x1</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <span class="id" title="var">x2</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#merge_s1"><span class="id" title="variable">merge_s1</span></a> <span class="id" title="var">s2'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <span class="id" title="var">x1</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <span class="id" title="var">s1'</span> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#merge_s1"><span class="id" title="variable">merge_s1</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="merge_path"><span class="id" title="lemma">merge_path</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="merge_sorted"><span class="id" title="lemma">merge_sorted</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_merge"><span class="id" title="lemma">perm_merge</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#perm_eql"><span class="id" title="abbreviation">perm_eql</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_merge"><span class="id" title="lemma">mem_merge</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.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#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_merge"><span class="id" title="lemma">size_merge</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="merge_uniq"><span class="id" title="lemma">merge_uniq</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</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#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="merge_sort_push"><span class="id" title="definition">merge_sort_push</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">ss</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.path.html#ss"><span class="id" title="variable">ss</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">ss'</span> | <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <span class="id" title="keyword">as</span> <span class="id" title="var">ss'</span> ⇒ <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">ss'</span><br/>
+&nbsp;&nbsp;| <span class="id" title="var">s2</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">ss'</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_push"><span class="id" title="definition">merge_sort_push</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <span class="id" title="var">s2</span>) <span class="id" title="var">ss'</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="merge_sort_pop"><span class="id" title="definition">merge_sort_pop</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">ss</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#ss"><span class="id" title="variable">ss</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">s2</span> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">ss'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_pop"><span class="id" title="definition">merge_sort_pop</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge"><span class="id" title="definition">merge</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <span class="id" title="var">s2</span>) <span class="id" title="var">ss'</span> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="merge_sort_rec"><span class="id" title="definition">merge_sort_rec</span></a> <span class="id" title="var">ss</span> <span class="id" title="var">s</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.ssreflect.seq.html#fcbb95c5c5fd941c49e06d09a4f5a316"><span class="id" title="notation">[::</span></a> <span class="id" title="var">x1</span><a class="idref" href="mathcomp.ssreflect.seq.html#fcbb95c5c5fd941c49e06d09a4f5a316"><span class="id" title="notation">,</span></a> <span class="id" title="var">x2</span> <a class="idref" href="mathcomp.ssreflect.seq.html#fcbb95c5c5fd941c49e06d09a4f5a316"><span class="id" title="notation">&amp;</span></a> <span class="id" title="var">s'</span><a class="idref" href="mathcomp.ssreflect.seq.html#fcbb95c5c5fd941c49e06d09a4f5a316"><span class="id" title="notation">]</span></a> <span class="id" title="keyword">then</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">s1</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <span class="id" title="var">x1</span> <span class="id" title="var">x2</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">[::</span></a> <span class="id" title="var">x1</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">;</span></a> <span class="id" title="var">x2</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">[::</span></a> <span class="id" title="var">x2</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">;</span></a> <span class="id" title="var">x1</span><a class="idref" href="mathcomp.ssreflect.seq.html#b2d6f6eec274c9f9919a378a42b5b183"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_rec"><span class="id" title="definition">merge_sort_rec</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_push"><span class="id" title="definition">merge_sort_push</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#ss"><span class="id" title="variable">ss</span></a>) <span class="id" title="var">s'</span><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_pop"><span class="id" title="definition">merge_sort_pop</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#ss"><span class="id" title="variable">ss</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="sort"><span class="id" title="definition">sort</span></a> := <a class="idref" href="mathcomp.ssreflect.path.html#merge_sort_rec"><span class="id" title="definition">merge_sort_rec</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sort_sorted"><span class="id" title="lemma">sort_sorted</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_sort"><span class="id" title="lemma">perm_sort</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#perm_eql"><span class="id" title="abbreviation">perm_eql</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_sort"><span class="id" title="lemma">mem_sort</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.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="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_sort"><span class="id" title="lemma">size_sort</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="sort_uniq"><span class="id" title="lemma">sort_uniq</span></a> <span class="id" title="var">s</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#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="perm_sortP"><span class="id" title="lemma">perm_sortP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</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.ssr.ssrbool.html#antisymmetric"><span class="id" title="definition">antisymmetric</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq.leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <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.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s1"><span class="id" title="variable">s1</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.path.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</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.ssreflect.path.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#SortSeq"><span class="id" title="section">SortSeq</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rev_sorted"><span class="id" title="lemma">rev_sorted</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">leT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">s</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#leT"><span class="id" title="variable">leT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.path.html#sorted"><span class="id" title="definition">sorted</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">y</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.path.html#leT"><span class="id" title="variable">leT</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ltn_sorted_uniq_leq"><span class="id" title="lemma">ltn_sorted_uniq_leq</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn"><span class="id" title="definition">ltn</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#leq"><span class="id" title="definition">leq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="iota_sorted"><span class="id" title="lemma">iota_sorted</span></a> <span class="id" title="var">i</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#leq"><span class="id" title="definition">leq</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#iota"><span class="id" title="definition">iota</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="iota_ltn_sorted"><span class="id" title="lemma">iota_ltn_sorted</span></a> <span class="id" title="var">i</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn"><span class="id" title="definition">ltn</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#iota"><span class="id" title="definition">iota</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>).<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ Function trajectories.  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="fpath"><span class="id" title="abbreviation">fpath</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/>
+<span class="id" title="keyword">Notation</span> <a name="fcycle"><span class="id" title="abbreviation">fcycle</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/>
+<span class="id" title="keyword">Notation</span> <a name="ufcycle"><span class="id" title="abbreviation">ufcycle</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.path.html#ucycle"><span class="id" title="definition">ucycle</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Trajectory"><span class="id" title="section">Trajectory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Trajectory.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Trajectory.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="traject"><span class="id" title="definition">traject</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <span class="id" title="var">n'</span> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="trajectS"><span class="id" title="lemma">trajectS</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="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.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="trajectSr"><span class="id" title="lemma">trajectSr</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) (<a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="last_traject"><span class="id" title="lemma">last_traject</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="traject_iteri"><span class="id" title="lemma">traject_iteri</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iteri"><span class="id" title="definition">iteri</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#rcons"><span class="id" title="definition">rcons</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">)</span></a>) <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_traject"><span class="id" title="lemma">size_traject</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="nth_traject"><span class="id" title="lemma">nth_traject</span></a> <span class="id" title="var">i</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#Trajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#Trajectory"><span class="id" title="section">Trajectory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="EqTrajectory"><span class="id" title="section">EqTrajectory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="EqTrajectory.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a name="EqTrajectory.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_fpath"><span class="id" title="lemma">eq_fpath</span></a> <span class="id" title="var">f'</span> : <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</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.ssreflect.path.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.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#f'"><span class="id" title="variable">f'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_fcycle"><span class="id" title="lemma">eq_fcycle</span></a> <span class="id" title="var">f'</span> : <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</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.ssreflect.path.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.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</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.ssreflect.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#f'"><span class="id" title="variable">f'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="fpathP"><span class="id" title="lemma">fpathP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#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">n</span><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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="fpath_traject"><span class="id" title="lemma">fpath_traject</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="looping"><span class="id" title="definition">looping</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="loopingP"><span class="id" title="lemma">loopingP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> :<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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>, <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#looping"><span class="id" title="definition">looping</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="trajectP"><span class="id" title="lemma">trajectP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> <span class="id" title="var">y</span> :<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#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="looping_uniq"><span class="id" title="lemma">looping_uniq</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</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.ssreflect.path.html#EqTrajectory.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#looping"><span class="id" title="definition">looping</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#n"><span class="id" title="variable">n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#EqTrajectory"><span class="id" title="section">EqTrajectory</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UniqCycle"><span class="id" title="section">UniqCycle</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="UniqCycle.n0"><span class="id" title="variable">n0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="UniqCycle.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a name="UniqCycle.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="UniqCycle.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="UniqCycle.Up"><span class="id" title="variable">Up</span></a> : <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#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_next"><span class="id" title="lemma">prev_next</span></a> : <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.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_prev"><span class="id" title="lemma">next_prev</span></a> : <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.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cycle_next"><span class="id" title="lemma">cycle_next</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cycle_prev"><span class="id" title="lemma">cycle_prev</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cycle_from_next"><span class="id" title="lemma">cycle_from_next</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">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cycle_from_prev"><span class="id" title="lemma">cycle_from_prev</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">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#cycle"><span class="id" title="definition">cycle</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_rot"><span class="id" title="lemma">next_rot</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</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.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_rot"><span class="id" title="lemma">prev_rot</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</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.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycle"><span class="id" title="section">UniqCycle</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UniqRotrCycle"><span class="id" title="section">UniqRotrCycle</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="UniqRotrCycle.n0"><span class="id" title="variable">n0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="UniqRotrCycle.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a name="UniqRotrCycle.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="UniqRotrCycle.Up"><span class="id" title="variable">Up</span></a> : <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#UniqRotrCycle.p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_rotr"><span class="id" title="lemma">next_rotr</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rotr"><span class="id" title="definition">rotr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.p"><span class="id" title="variable">p</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.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.p"><span class="id" title="variable">p</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_rotr"><span class="id" title="lemma">prev_rotr</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rotr"><span class="id" title="definition">rotr</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.n0"><span class="id" title="variable">n0</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.p"><span class="id" title="variable">p</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.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle.p"><span class="id" title="variable">p</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#UniqRotrCycle"><span class="id" title="section">UniqRotrCycle</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UniqCycleRev"><span class="id" title="section">UniqCycleRev</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="UniqCycleRev.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycleRev.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_rev"><span class="id" title="lemma">prev_rev</span></a> <span class="id" title="var">p</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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_rev"><span class="id" title="lemma">next_rev</span></a> <span class="id" title="var">p</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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#UniqCycleRev"><span class="id" title="section">UniqCycleRev</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="MapPath"><span class="id" title="section">MapPath</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MapPath.T"><span class="id" title="variable">T</span></a> <a name="MapPath.T'"><span class="id" title="variable">T'</span></a> : <span class="id" title="keyword">Type</span>) (<a name="MapPath.h"><span class="id" title="variable">h</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#T'"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="MapPath.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="MapPath.e'"><span class="id" title="variable">e'</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T'"><span class="id" title="variable">T'</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="rel_base"><span class="id" title="definition">rel_base</span></a> (<span class="id" title="var">b</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.ssreflect.path.html#MapPath.T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</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.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#b"><span class="id" title="variable">b</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#MapPath.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y'"><span class="id" title="variable">y'</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="map_path"><span class="id" title="lemma">map_path</span></a> <span class="id" title="var">b</span> <span class="id" title="var">x'</span> <span class="id" title="var">p'</span> (<span class="id" title="var">Bb</span> : <a class="idref" href="mathcomp.ssreflect.path.html#rel_base"><span class="id" title="definition">rel_base</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#b"><span class="id" title="variable">b</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#has"><span class="id" title="definition">has</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#preim"><span class="id" title="definition">preim</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#b"><span class="id" title="variable">b</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#MapPath"><span class="id" title="section">MapPath</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="MapEqPath"><span class="id" title="section">MapEqPath</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MapEqPath.T"><span class="id" title="variable">T</span></a> <a name="MapEqPath.T'"><span class="id" title="variable">T'</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a name="MapEqPath.h"><span class="id" title="variable">h</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#T'"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="MapEqPath.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) (<a name="MapEqPath.e'"><span class="id" title="variable">e'</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T'"><span class="id" title="variable">T'</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Hypothesis</span> <a name="MapEqPath.Ih"><span class="id" title="variable">Ih</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem2_map"><span class="id" title="lemma">mem2_map</span></a> <span class="id" title="var">x'</span> <span class="id" title="var">y'</span> <span class="id" title="var">p'</span> : <a class="idref" href="mathcomp.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#mem2"><span class="id" title="definition">mem2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p'"><span class="id" title="variable">p'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y'"><span class="id" title="variable">y'</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="next_map"><span class="id" title="lemma">next_map</span></a> <span class="id" title="var">p</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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#next"><span class="id" title="definition">next</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prev_map"><span class="id" title="lemma">prev_map</span></a> <span class="id" title="var">p</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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.path.html#MapEqPath.h"><span class="id" title="variable">h</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#prev"><span class="id" title="definition">prev</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#MapEqPath"><span class="id" title="section">MapEqPath</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="fun_base"><span class="id" title="definition">fun_base</span></a> (<span class="id" title="var">T</span> <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">h</span> : <a class="idref" href="mathcomp.ssreflect.path.html#T'"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">f</span> <span class="id" title="var">f'</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#rel_base"><span class="id" title="definition">rel_base</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#h"><span class="id" title="variable">h</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#f"><span class="id" title="variable">f</span></a>) (<a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#f'"><span class="id" title="variable">f'</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CycleArc"><span class="id" title="section">CycleArc</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CycleArc.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#CycleArc.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="arc"><span class="id" title="definition">arc</span></a> <span class="id" title="var">p</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">px</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.seq.html#take"><span class="id" title="definition">take</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#px"><span class="id" title="variable">px</span></a>) <a class="idref" href="mathcomp.ssreflect.path.html#px"><span class="id" title="variable">px</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="arc_rot"><span class="id" title="lemma">arc_rot</span></a> <span class="id" title="var">i</span> <span class="id" title="var">p</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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#arc"><span class="id" title="definition">arc</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#arc"><span class="id" title="definition">arc</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="left_arc"><span class="id" title="lemma">left_arc</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> (<span class="id" title="var">p</span> := <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) :<br/>
+&nbsp;&nbsp;<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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#arc"><span class="id" title="definition">arc</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="right_arc"><span class="id" title="lemma">right_arc</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> (<span class="id" title="var">p</span> := <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>) :<br/>
+&nbsp;&nbsp;<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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#arc"><span class="id" title="definition">arc</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="rot_to_arc_spec"><span class="id" title="inductive">rot_to_arc_spec</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :=<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a name="RotToArcSpec"><span class="id" title="constructor">RotToArcSpec</span></a> <span class="id" title="var">i</span> <span class="id" title="var">p1</span> <span class="id" title="var">p2</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</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.path.html#arc"><span class="id" title="definition">arc</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a><br/>
+&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;&amp; <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</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.path.html#arc"><span class="id" title="definition">arc</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a><br/>
+&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;&amp; <a class="idref" href="mathcomp.ssreflect.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p1"><span class="id" title="variable">p1</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p2"><span class="id" title="variable">p2</span></a> :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.path.html#rot_to_arc_spec"><span class="id" title="inductive">rot_to_arc_spec</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rot_to_arc"><span class="id" title="lemma">rot_to_arc</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/>
+&nbsp;&nbsp;<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#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.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.ssreflect.path.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#rot_to_arc_spec"><span class="id" title="inductive">rot_to_arc_spec</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#y"><span class="id" title="variable">y</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.path.html#CycleArc"><span class="id" title="section">CycleArc</span></a>.<br/>
+
+<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.ssreflect.path.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)