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.tuple.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 465 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.tuple.html b/docs/htmldoc/mathcomp.ssreflect.tuple.html
new file mode 100644
index 0000000..1dd43d4
--- /dev/null
+++ b/docs/htmldoc/mathcomp.ssreflect.tuple.html
@@ -0,0 +1,465 @@
+<!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.tuple</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.ssreflect.tuple</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/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Tuples, i.e., sequences with a fixed (known) length. We define:            
+         n.-tuple T == the type of n-tuples of elements of type T.          
+       [tuple of s] == the tuple whose underlying sequence (value) is s.    
+                       The size of s must be known: specifically, Coq must  
+                       be able to infer a Canonical tuple projecting on s.  
+         in_tuple s == the (size s)-tuple with value s.                     
+            [tuple] == the empty tuple.                                     
+ [tuple x1; ..; xn] == the explicit n.-tuple &lt;x1; ..; xn&gt;.                  
+  [tuple E | i &lt; n] == the n.-tuple with general term E (i : 'I_n is bound  
+                       in E).                                               
+        tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n.  
+ As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be 
+ applied to t : n.-tuple T; we provide a few specialized instances when     
+ avoids the need for a default value.                                       
+            tsize t == the size of t (the n in n.-tuple T)                  
+           tnth t i == the i'th component of t, where i : 'I_n.             
+         [tnth t i] == the i'th component of t, where i : nat and i &lt; n     
+                       is convertible to true.                              
+            thead t == the first element of t, when n is m.+1 for some m.   
+ Most seq constructors (cons, behead, cat, rcons, belast, take, drop, rot,  
+ map, ...) can be used to build tuples via the [tuple of s] construct.      
+   Tuples are actually a subType of seq, and inherit all combinatorial      
+ structures, including the finType structure.                               
+   Some useful lemmas and definitions:                                      
+     tuple0 : [tuple] is the only 0.-tuple                                  
+     tupleP : elimination view for n.+1.-tuple                              
+     ord_tuple n : the n.-tuple of all i : 'I_n                              
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Def"><span class="id" title="section">Def</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Def.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="Def.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="tuple_of"><span class="id" title="record">tuple_of</span></a> : <span class="id" title="keyword">Type</span> := <a name="Tuple"><span class="id" title="constructor">Tuple</span></a> {<a name="tval"><span class="id" title="projection">tval</span></a> :&gt; <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.T"><span class="id" title="variable">T</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tval"><span class="id" title="method">tval</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>}.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tval"><span class="id" title="projection">tval</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tsize"><span class="id" title="definition">tsize</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="size_tuple"><span class="id" title="lemma">size_tuple</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_default"><span class="id" title="lemma">tnth_default</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a> <a class="idref" href="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.tuple.html#Def.T"><span class="id" title="variable">T</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tnth"><span class="id" title="definition">tnth</span></a> <span class="id" title="var">t</span> <span class="id" title="var">i</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth_default"><span class="id" title="lemma">tnth_default</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_nth"><span class="id" title="lemma">tnth_nth</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="map_tnth_enum"><span class="id" title="lemma">map_tnth_enum</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="eq_from_tnth"><span class="id" title="lemma">eq_from_tnth</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t1"><span class="id" title="variable">t1</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.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t2"><span class="id" title="variable">t2</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.tuple.html#t1"><span class="id" title="variable">t1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t2"><span class="id" title="variable">t2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tuple"><span class="id" title="definition">tuple</span></a> <span class="id" title="var">t</span> <span class="id" title="var">mkT</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.tuple.html#mkT"><span class="id" title="variable">mkT</span></a> (<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <span class="id" title="var">_</span> <span class="id" title="var">tP</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def.n"><span class="id" title="variable">n</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">tP</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tupleE"><span class="id" title="lemma">tupleE</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple"><span class="id" title="definition">tuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sP</span> ⇒ @<a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#sP"><span class="id" title="variable">sP</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#Def"><span class="id" title="section">Def</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">&quot;</span></a>n .-tuple" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_of"><span class="id" title="record">tuple_of</span></a> <span class="id" title="var">n</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "n .-tuple") : <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="ac6e2e021da54ee5885e636c6c87966d"><span class="id" title="notation">&quot;</span></a>{ 'tuple' n 'of' T }" := (<span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <span class="id" title="var">T</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">&quot;</span></a>[ 'tuple' 'of' s ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple"><span class="id" title="definition">tuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">sP</span> ⇒ @<a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">s</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#sP"><span class="id" title="variable">sP</span></a>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple'  'of'  s ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="7f12dc1a1a5a7ee83220e323c866673f"><span class="id" title="notation">&quot;</span></a>[ 'tnth' t i ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <span class="id" title="var">t</span> (@<a class="idref" href="mathcomp.ssreflect.fintype.html#Ordinal"><span class="id" title="constructor">Ordinal</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tsize"><span class="id" title="definition">tsize</span></a> <span class="id" title="var">t</span>) <span class="id" title="var">i</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#erefl"><span class="id" title="abbreviation">erefl</span></a> <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/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">t</span>, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "[ 'tnth'  t  i ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">nil_tuple</span> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#isT"><span class="id" title="definition">isT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">cons_tuple</span> <span class="id" title="var">n</span> <span class="id" title="var">T</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#valP"><span class="id" title="lemma">valP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><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.tuple.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.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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>).<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="b96c5fac4ea7ac478a42dc9d76e9dbb3"><span class="id" title="notation">&quot;</span></a>[ 'tuple' x1 ; .. ; xn ]" := <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <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.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <span class="id" title="var">xn</span><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a> ..<a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple' '['  x1 ; '/'  .. ; '/'  xn ']' ]")<br/>
+&nbsp;&nbsp;: <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">&quot;</span></a>[ 'tuple' ]" := <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a><br/>
+  (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'tuple' ]") : <span class="id" title="var">form_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CastTuple"><span class="id" title="section">CastTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CastTuple.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="in_tuple"><span class="id" title="definition">in_tuple</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#eqxx"><span class="id" title="abbreviation">eqxx</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.tuple.html#s"><span class="id" title="variable">s</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tcast"><span class="id" title="definition">tcast</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span>: <span class="id" title="var">erefl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">_</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> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tcastE"><span class="id" title="lemma">tcastE</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> <span class="id" title="var">i</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#cast_ord"><span class="id" title="definition">cast_ord</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tcast_id"><span class="id" title="lemma">tcast_id</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">eq_nn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_nn"><span class="id" title="variable">eq_nn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tcastK"><span class="id" title="lemma">tcastK</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</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.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>)).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tcastKV"><span class="id" title="lemma">tcastKV</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</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.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>)) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tcast_trans"><span class="id" title="lemma">tcast_trans</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> <span class="id" title="var">p</span> (<span class="id" title="var">eq_mn</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a>) (<span class="id" title="var">eq_np</span> : <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#p"><span class="id" title="variable">p</span></a>) <span class="id" title="var">t</span>:<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#etrans"><span class="id" title="definition">etrans</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_np"><span class="id" title="variable">eq_np</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_np"><span class="id" title="variable">eq_np</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#eq_mn"><span class="id" title="variable">eq_mn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tvalK"><span class="id" title="lemma">tvalK</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tcast"><span class="id" title="definition">tcast</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#esym"><span class="id" title="definition">esym</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#size_tuple"><span class="id" title="lemma">size_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>)) <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="in_tupleE"><span class="id" title="lemma">in_tupleE</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple.T"><span class="id" title="variable">T</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#CastTuple"><span class="id" title="section">CastTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="SeqTuple"><span class="id" title="section">SeqTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="SeqTuple.n"><span class="id" title="variable">n</span></a> <a name="SeqTuple.m"><span class="id" title="variable">m</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="SeqTuple.T"><span class="id" title="variable">T</span></a> <a name="SeqTuple.U"><span class="id" title="variable">U</span></a> <a name="SeqTuple.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rcons_tupleP"><span class="id" title="lemma">rcons_tupleP</span></a> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#SeqTuple.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>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rcons_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rcons_tupleP"><span class="id" title="lemma">rcons_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="nseq_tupleP"><span class="id" title="lemma">nseq_tupleP</span></a> <span class="id" title="var">x</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#nseq"><span class="id" title="definition">nseq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">nseq_tuple</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#nseq_tupleP"><span class="id" title="lemma">nseq_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="iota_tupleP"><span class="id" title="lemma">iota_tupleP</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.seq.html#iota"><span class="id" title="definition">iota</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">iota_tuple</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#iota_tupleP"><span class="id" title="lemma">iota_tupleP</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="behead_tupleP"><span class="id" title="lemma">behead_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">behead_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#behead_tupleP"><span class="id" title="lemma">behead_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="belast_tupleP"><span class="id" title="lemma">belast_tupleP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">belast_tuple</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#belast_tupleP"><span class="id" title="lemma">belast_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cat_tupleP"><span class="id" title="lemma">cat_tupleP</span></a> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</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.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#2ac9001c05ad5bd2f6d5f68e59f48fbb"><span class="id" title="notation">++</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">cat_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#cat_tupleP"><span class="id" title="lemma">cat_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="take_tupleP"><span class="id" title="lemma">take_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#minn"><span class="id" title="definition">minn</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">take_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#take_tupleP"><span class="id" title="lemma">take_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="drop_tupleP"><span class="id" title="lemma">drop_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">drop_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#drop_tupleP"><span class="id" title="lemma">drop_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rev_tupleP"><span class="id" title="lemma">rev_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rev_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rev_tupleP"><span class="id" title="lemma">rev_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rot_tupleP"><span class="id" title="lemma">rot_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rot_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rot_tupleP"><span class="id" title="lemma">rot_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="rotr_tupleP"><span class="id" title="lemma">rotr_tupleP</span></a> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</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.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">rotr_tuple</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#rotr_tupleP"><span class="id" title="lemma">rotr_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="map_tupleP"><span class="id" title="lemma">map_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</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.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">map_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#map_tupleP"><span class="id" title="lemma">map_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="scanl_tupleP"><span class="id" title="lemma">scanl_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#scanl"><span class="id" title="definition">scanl</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">scanl_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#scanl_tupleP"><span class="id" title="lemma">scanl_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pairmap_tupleP"><span class="id" title="lemma">pairmap_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pairmap"><span class="id" title="definition">pairmap</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pairmap_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#pairmap_tupleP"><span class="id" title="lemma">pairmap_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="zip_tupleP"><span class="id" title="lemma">zip_tupleP</span></a> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.U"><span class="id" title="variable">U</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.seq.html#zip"><span class="id" title="definition">zip</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">zip_tuple</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#zip_tupleP"><span class="id" title="lemma">zip_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="allpairs_tupleP"><span class="id" title="lemma">allpairs_tupleP</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.U"><span class="id" title="variable">U</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.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#allpairs"><span class="id" title="definition">allpairs</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.m"><span class="id" title="variable">m</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">allpairs_tuple</span> <span class="id" title="var">f</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#allpairs_tupleP"><span class="id" title="lemma">allpairs_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="thead"><span class="id" title="definition">thead</span></a> (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ord0"><span class="id" title="definition">ord0</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth0"><span class="id" title="lemma">tnth0</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ord0"><span class="id" title="definition">ord0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="theadE"><span class="id" title="lemma">theadE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#thead"><span class="id" title="definition">thead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tuple0"><span class="id" title="lemma">tuple0</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#all_equal_to"><span class="id" title="definition">all_equal_to</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> 0<a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.T"><span class="id" title="variable">T</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">CoInductive</span> <a name="tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.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="Tuple1spec"><span class="id" title="constructor">Tuple1spec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tupleP"><span class="id" title="lemma">tupleP</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple1_spec"><span class="id" title="inductive">tuple1_spec</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#u"><span class="id" title="variable">u</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_map"><span class="id" title="lemma">tnth_map</span></a> <span class="id" title="var">f</span> <span class="id" title="var">t</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple.rT"><span class="id" title="variable">rT</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#SeqTuple"><span class="id" title="section">SeqTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_behead"><span class="id" title="lemma">tnth_behead</span></a> <span class="id" title="var">n</span> <span class="id" title="var">T</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">i</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#inord"><span class="id" title="definition">inord</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tuple_eta"><span class="id" title="lemma">tuple_eta</span></a> <span class="id" title="var">n</span> <span class="id" title="var">T</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#thead"><span class="id" title="definition">thead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#behead"><span class="id" title="definition">behead</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Section</span> <a name="TupleQuantifiers"><span class="id" title="section">TupleQuantifiers</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="TupleQuantifiers.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="TupleQuantifiers.T"><span class="id" title="variable">T</span></a> : <span class="id" title="keyword">Type</span>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">a</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.tuple.html#TupleQuantifiers.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="forallb_tnth"><span class="id" title="lemma">forallb_tnth</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">∀</span></a> <span class="id" title="var">i</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="existsb_tnth"><span class="id" title="lemma">existsb_tnth</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">∃</span></a> <span class="id" title="var">i</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#has"><span class="id" title="definition">has</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="all_tnthP"><span class="id" title="lemma">all_tnthP</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</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.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="has_tnthP"><span class="id" title="lemma">has_tnthP</span></a> <span class="id" title="var">a</span> <span class="id" title="var">t</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">i</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.tuple.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>)) (<a class="idref" href="mathcomp.ssreflect.seq.html#has"><span class="id" title="definition">has</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#TupleQuantifiers"><span class="id" title="section">TupleQuantifiers</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="EqTuple"><span class="id" title="section">EqTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="EqTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="EqTuple.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/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tuple_eqMixin"><span class="id" title="definition">tuple_eqMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_eqMixin"><span class="id" title="definition">tuple_eqMixin</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_predType</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mkPredType"><span class="id" title="definition">mkPredType</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#mem_seq"><span class="id" title="definition">mem_seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="memtE"><span class="id" title="lemma">memtE</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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.tuple.html#tval"><span class="id" title="projection">tval</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="mem_tnth"><span class="id" title="lemma">mem_tnth</span></a> <span class="id" title="var">i</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="memt_nth"><span class="id" title="lemma">memt_nth</span></a> <span class="id" title="var">x0</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnthP"><span class="id" title="lemma">tnthP</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#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">i</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.tuple.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.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#t"><span class="id" title="variable">t</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="seq_tnthP"><span class="id" title="lemma">seq_tnthP</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple.T"><span class="id" title="variable">T</span></a>) <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#in_tuple"><span class="id" title="definition">in_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.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.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#EqTuple"><span class="id" title="section">EqTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tuple_choiceMixin"><span class="id" title="definition">tuple_choiceMixin</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_choiceType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_choiceMixin"><span class="id" title="definition">tuple_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="tuple_countMixin"><span class="id" title="definition">tuple_countMixin</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_countType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>) (<a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_countMixin"><span class="id" title="definition">tuple_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subCountType</span> <span class="id" title="var">n</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/>
+<span class="id" title="keyword">Section</span> <a name="FinTupleSig.FinTupleSig"><span class="id" title="section">FinTupleSig</span></a>.<br/>
+<span class="id" title="keyword">Variables</span> (<a name="FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/>
+<span class="id" title="keyword">Parameter</span> <a name="FinTupleSig.enum"><span class="id" title="axiom">enum</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.tuple.html#FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Axiom</span> <a name="FinTupleSig.enumP"><span class="id" title="axiom">enumP</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.axiom"><span class="id" title="definition">Finite.axiom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.enum"><span class="id" title="axiom">enum</span></a>.<br/>
+<span class="id" title="keyword">Axiom</span> <a name="FinTupleSig.size_enum"><span class="id" title="axiom">size_enum</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.tuple.html#FinTupleSig.enum"><span class="id" title="axiom">enum</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig.n"><span class="id" title="variable">n</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig.FinTupleSig"><span class="id" title="section">FinTupleSig</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="FinTuple"><span class="id" title="module">FinTuple</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTupleSig"><span class="id" title="module">FinTupleSig</span></a>.<br/>
+<span class="id" title="keyword">Section</span> <a name="FinTuple.FinTuple"><span class="id" title="section">FinTuple</span></a>.<br/>
+<span class="id" title="keyword">Variables</span> (<a name="FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="FinTuple.enum"><span class="id" title="definition">enum</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.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">extend</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#flatten"><span class="id" title="definition">flatten</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#cons"><span class="id" title="constructor">cons</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#e"><span class="id" title="variable">e</span></a>)) <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.seq.html#pmap"><span class="id" title="definition">pmap</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</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.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#extend"><span class="id" title="variable">extend</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FinTuple.enumP"><span class="id" title="lemma">enumP</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.axiom"><span class="id" title="definition">Finite.axiom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.enum"><span class="id" title="definition">enum</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FinTuple.size_enum"><span class="id" title="lemma">size_enum</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.tuple.html#FinTuple.enum"><span class="id" title="definition">enum</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple.FinTuple"><span class="id" title="section">FinTuple</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#FinTuple"><span class="id" title="module">FinTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UseFinTuple"><span class="id" title="section">UseFinTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="UseFinTuple.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_finMixin</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinMixin"><span class="id" title="abbreviation">FinMixin</span></a> (@<a class="idref" href="mathcomp.ssreflect.tuple.html#enumP"><span class="id" title="axiom">FinTuple.enumP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#tuple_finMixin"><span class="id" title="definition">tuple_finMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">tuple_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_tuple"><span class="id" title="lemma">card_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#74a34ed1f9b36f83662203527a970b09"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#74a34ed1f9b36f83662203527a970b09"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="enum_tupleP"><span class="id" title="lemma">enum_tupleP</span></a> (<span class="id" title="var">A</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.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</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.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">enum_tuple</span> <span class="id" title="var">A</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#enum_tupleP"><span class="id" title="lemma">enum_tupleP</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#A"><span class="id" title="variable">A</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="ord_tuple"><span class="id" title="definition">ord_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#Tuple"><span class="id" title="constructor">Tuple</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#introT"><span class="id" title="lemma">introT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#eqP"><span class="id" title="lemma">eqP</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#size_enum_ord"><span class="id" title="lemma">size_enum_ord</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a>)).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="val_ord_tuple"><span class="id" title="lemma">val_ord_tuple</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tuple_map_ord"><span class="id" title="lemma">tuple_map_ord</span></a> <span class="id" title="var">U</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#U"><span class="id" title="variable">U</span></a>) : <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_ord_tuple"><span class="id" title="lemma">tnth_ord_tuple</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UseFinTuple.ImageTuple"><span class="id" title="section">ImageTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> : <span class="id" title="keyword">Type</span>) (<a name="UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.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.tuple.html#T'"><span class="id" title="variable">T'</span></a>) (<a name="UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">image_tuple</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#image"><span class="id" title="abbreviation">image</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">codom_tuple</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.T'"><span class="id" title="variable">T'</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple.f"><span class="id" title="variable">f</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.ImageTuple"><span class="id" title="section">ImageTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="UseFinTuple.MkTuple"><span class="id" title="section">MkTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="UseFinTuple.MkTuple.T'"><span class="id" title="variable">T'</span></a> : <span class="id" title="keyword">Type</span>) (<a name="UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a> <a class="idref" href="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.tuple.html#T'"><span class="id" title="variable">T'</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="mktuple"><span class="id" title="definition">mktuple</span></a> := <a class="idref" href="mathcomp.ssreflect.tuple.html#map_tuple"><span class="id" title="definition">map_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#ord_tuple"><span class="id" title="definition">ord_tuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_mktuple"><span class="id" title="lemma">tnth_mktuple</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="nth_mktuple"><span class="id" title="lemma">nth_mktuple</span></a> <span class="id" title="var">x0</span> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#x0"><span class="id" title="variable">x0</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.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.tuple.html#UseFinTuple.MkTuple.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#i"><span class="id" title="variable">i</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple.MkTuple"><span class="id" title="section">MkTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#UseFinTuple"><span class="id" title="section">UseFinTuple</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="1bdc3d6f63dc0019ce17772415ee5798"><span class="id" title="notation">&quot;</span></a>[ 'tuple' F | i &lt; n ]" := (<a class="idref" href="mathcomp.ssreflect.tuple.html#mktuple"><span class="id" title="definition">mktuple</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a> ⇒ <span class="id" title="var">F</span>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/>
+&nbsp;&nbsp;&nbsp;<span class="id" title="var">format</span> "[ '[hv' 'tuple'  F '/'   |  i  &lt;  n ] ']'") : <span class="id" title="var">form_scope</span>.<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.tuple.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)