diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.fingraph.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.fingraph.html | 651 |
1 files changed, 651 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.fingraph.html b/docs/htmldoc/mathcomp.ssreflect.fingraph.html new file mode 100644 index 0000000..80bfb6e --- /dev/null +++ b/docs/htmldoc/mathcomp.ssreflect.fingraph.html @@ -0,0 +1,651 @@ +<!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.fingraph</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.ssreflect.fingraph</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</span><br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This file develops the theory of finite graphs represented by an "edge" + relation over a finType T; this mainly amounts to the theory of the + transitive closure of such relations. + For g : T -> seq T, e : rel T and f : T -> T we define: + grel g == the adjacency relation y \in g x of the graph g. + rgraph e == the graph (x |-> enum (e x)) of the relation e. + dfs g n v x == the list of points traversed by a depth-first search of + the g, at depth n, starting from x, and avoiding v. + dfs_path g v x y <-> there is a path from x to y in g \ v. + connect e == the transitive closure of e (computed by dfs). + connect_sym e <-> connect e is symmetric, hence an equivalence relation. + root e x == a representative of connect e x, which is the component + of x in the transitive closure of e. + roots e == the codomain predicate of root e. + n_comp e a == the number of e-connected components of a, when a is + e-closed and connect e is symmetric. + equivalence classes of connect e if connect_sym e holds. + closed e a == the collective predicate a is e-invariant. + closure e a == the e-closure of a (the image of a under connect e). + rel_adjunction h e e' a <-> in the e-closed domain a, h is the left part + of an adjunction from e to another relation e'. + fconnect f == connect (frel f), i.e., "connected under f iteration". + froot f x == root (frel f) x, the root of the orbit of x under f. + froots f == roots (frel f) == orbit representatives for f. + orbit f x == lists the f-orbit of x. + findex f x y == index of y in the f-orbit of x. + order f x == size (cardinal) of the f-orbit of x. + order_set f n == elements of f-order n. + finv f == the inverse of f, if f is injective. + := finv f x := iter (order x).-1 f x. + fcard f a == number of orbits of f in a, provided a is f-invariant + f is one-to-one. + fclosed f a == the collective predicate a is f-invariant. + fclosure f a == the closure of a under f iteration. + fun_adjunction == rel_adjunction (frel f). +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="grel"><span class="id" title="definition">grel</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<span class="id" title="var">g</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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#82abed2919e25bf64cb56067d0f5feee"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Decidable connectivity in finite types. +</div> +<div class="code"> +<span class="id" title="keyword">Section</span> <a name="Connect"><span class="id" title="section">Connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Connect.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">Section</span> <a name="Connect.Dfs"><span class="id" title="section">Dfs</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Connect.Dfs.g"><span class="id" title="variable">g</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">v</span> <span class="id" title="var">w</span> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="dfs"><span class="id" title="definition">dfs</span></a> <span class="id" title="var">n</span> <span class="id" title="var">v</span> <span class="id" title="var">x</span> :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a><br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.seq.html#foldl"><span class="id" title="definition">foldl</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <span class="id" title="var">n'</span>) (<a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#v"><span class="id" title="variable">v</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.Dfs.g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="subset_dfs"><span class="id" title="lemma">subset_dfs</span></a> <span class="id" title="var">n</span> <span class="id" title="var">v</span> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldl"><span class="id" title="definition">foldl</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Inductive</span> <a name="dfs_path"><span class="id" title="inductive">dfs_path</span></a> <span class="id" title="var">v</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="keyword">Prop</span> :=<br/> + <a name="DfsPath"><span class="id" title="constructor">DfsPath</span></a> <span class="id" title="var">p</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#grel"><span class="id" title="definition">grel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.Dfs.g"><span class="id" title="variable">g</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> & <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> & <a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">disjoint</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="dfs_pathP"><span class="id" title="lemma">dfs_pathP</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">v</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs_path"><span class="id" title="inductive">dfs_path</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="dfsP"><span class="id" title="lemma">dfsP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#grel"><span class="id" title="definition">grel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.Dfs.g"><span class="id" title="variable">g</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.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.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.Dfs"><span class="id" title="section">Dfs</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Connect.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rgraph"><span class="id" title="definition">rgraph</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgraphK"><span class="id" title="lemma">rgraphK</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#grel"><span class="id" title="definition">grel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#rgraph"><span class="id" title="definition">rgraph</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="connect"><span class="id" title="definition">connect</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#rgraph"><span class="id" title="definition">rgraph</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.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.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><span class="id" title="notation">[::]</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">connect_app_pred</span> <span class="id" title="var">x</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ApplicativePred"><span class="id" title="definition">ApplicativePred</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connectP"><span class="id" title="lemma">connectP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect_trans"><span class="id" title="lemma">connect_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect0"><span class="id" title="lemma">connect0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_connect0"><span class="id" title="lemma">eq_connect0</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect1"><span class="id" title="lemma">connect1</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="path_connect"><span class="id" title="lemma">path_connect</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#subpred"><span class="id" title="definition">subpred</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#p"><span class="id" title="variable">p</span></a>)) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="root"><span class="id" title="definition">root</span></a> <span class="id" title="var">x</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#odflt"><span class="id" title="abbreviation">odflt</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#pick"><span class="id" title="definition">pick</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="roots"><span class="id" title="definition">roots</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.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">roots_pred</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ApplicativePred"><span class="id" title="definition">ApplicativePred</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="n_comp_mem"><span class="id" title="definition">n_comp_mem</span></a> (<span class="id" title="var">m_a</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem_pred"><span class="id" title="inductive">mem_pred</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predI"><span class="id" title="definition">predI</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect_root"><span class="id" title="lemma">connect_root</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="connect_sym"><span class="id" title="definition">connect_sym</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Connect.sym_e"><span class="id" title="variable">sym_e</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_connect"><span class="id" title="lemma">same_connect</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#left_transitive"><span class="id" title="definition">left_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_connect_r"><span class="id" title="lemma">same_connect_r</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#right_transitive"><span class="id" title="definition">right_transitive</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_connect1"><span class="id" title="lemma">same_connect1</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_connect1r"><span class="id" title="lemma">same_connect1r</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rootP"><span class="id" title="lemma">rootP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="root_root"><span class="id" title="lemma">root_root</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="roots_root"><span class="id" title="lemma">roots_root</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="root_connect"><span class="id" title="lemma">root_connect</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="closed_mem"><span class="id" title="definition">closed_mem</span></a> <span class="id" title="var">m_a</span> := <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="closure_mem"><span class="id" title="definition">closure_mem</span></a> <span class="id" title="var">m_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.fingraph.html#Connect.T"><span class="id" title="variable">T</span></a> :=<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#disjoint"><span class="id" title="definition">disjoint</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.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Connect"><span class="id" title="section">Connect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">connect0</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="n_comp"><span class="id" title="abbreviation">n_comp</span></a> <span class="id" title="var">e</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp_mem"><span class="id" title="definition">n_comp_mem</span></a> <span class="id" title="var">e</span> (<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> <span class="id" title="var">a</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="closed"><span class="id" title="abbreviation">closed</span></a> <span class="id" title="var">e</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closed_mem"><span class="id" title="definition">closed_mem</span></a> <span class="id" title="var">e</span> (<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> <span class="id" title="var">a</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="closure"><span class="id" title="abbreviation">closure</span></a> <span class="id" title="var">e</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closure_mem"><span class="id" title="definition">closure_mem</span></a> <span class="id" title="var">e</span> (<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> <span class="id" title="var">a</span>)).<br/> + +<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="fconnect"><span class="id" title="abbreviation">fconnect</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="froot"><span class="id" title="abbreviation">froot</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="froots"><span class="id" title="abbreviation">froots</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <span class="id" title="var">f</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp_mem"><span class="id" title="definition">n_comp_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="fcard"><span class="id" title="abbreviation">fcard</span></a> <span class="id" title="var">f</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <span class="id" title="var">f</span> (<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> <span class="id" title="var">a</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="fclosed"><span class="id" title="abbreviation">fclosed</span></a> <span class="id" title="var">f</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>) <span class="id" title="var">a</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="fclosure"><span class="id" title="abbreviation">fclosure</span></a> <span class="id" title="var">f</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closure"><span class="id" title="abbreviation">closure</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#coerced_frel"><span class="id" title="abbreviation">coerced_frel</span></a> <span class="id" title="var">f</span>) <span class="id" title="var">a</span>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="EqConnect"><span class="id" title="section">EqConnect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="EqConnect.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#EqConnect.T"><span class="id" title="variable">T</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.fingraph.html#EqConnect.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect_sub"><span class="id" title="lemma">connect_sub</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#subrel"><span class="id" title="definition">subrel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#subrel"><span class="id" title="definition">subrel</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="relU_sym"><span class="id" title="lemma">relU_sym</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#relU"><span class="id" title="definition">relU</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_connect"><span class="id" title="lemma">eq_connect</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_n_comp"><span class="id" title="lemma">eq_n_comp</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp_mem"><span class="id" title="definition">n_comp_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp_mem"><span class="id" title="definition">n_comp_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_n_comp_r"><span class="id" title="lemma">eq_n_comp_r</span></a> {<span class="id" title="var">e</span>} <span class="id" title="var">a</span> <span class="id" title="var">a'</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a'"><span class="id" title="variable">a'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a'"><span class="id" title="variable">a'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="n_compC"><span class="id" title="lemma">n_compC</span></a> <span class="id" title="var">a</span> <span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#EqConnect.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.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">predC</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_root"><span class="id" title="lemma">eq_root</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_roots"><span class="id" title="lemma">eq_roots</span></a> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#roots"><span class="id" title="definition">roots</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#e'"><span class="id" title="variable">e'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#EqConnect"><span class="id" title="section">EqConnect</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Closure"><span class="id" title="section">Closure</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Closure.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Closure.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Closure.sym_e"><span class="id" title="variable">sym_e</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</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.fingraph.html#Closure.T"><span class="id" title="variable">T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_connect_rev"><span class="id" title="lemma">same_connect_rev</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="intro_closed"><span class="id" title="lemma">intro_closed</span></a> <span class="id" title="var">a</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="closed_connect"><span class="id" title="lemma">closed_connect</span></a> <span class="id" title="var">a</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="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.fingraph.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.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="connect_closed"><span class="id" title="lemma">connect_closed</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="predC_closed"><span class="id" title="lemma">predC_closed</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">predC</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="closure_closed"><span class="id" title="lemma">closure_closed</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closure"><span class="id" title="abbreviation">closure</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="mem_closure"><span class="id" title="lemma">mem_closure</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#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#closure"><span class="id" title="abbreviation">closure</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="subset_closure"><span class="id" title="lemma">subset_closure</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#closure"><span class="id" title="abbreviation">closure</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="n_comp_closure2"><span class="id" title="lemma">n_comp_closure2</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#closure"><span class="id" title="abbreviation">closure</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#pred2"><span class="id" title="definition">pred2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</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="n_comp_connect"><span class="id" title="lemma">n_comp_connect</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure"><span class="id" title="section">Closure</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Orbit"><span class="id" title="section">Orbit</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Orbit.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Orbit.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="order"><span class="id" title="definition">order</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="orbit"><span class="id" title="definition">orbit</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="findex"><span class="id" title="definition">findex</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.ssreflect.seq.html#index"><span class="id" title="definition">index</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="finv"><span class="id" title="definition">finv</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_iter"><span class="id" title="lemma">fconnect_iter</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</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.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect1"><span class="id" title="lemma">fconnect1</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_finv"><span class="id" title="lemma">fconnect_finv</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="orderSpred"><span class="id" title="lemma">orderSpred</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="size_orbit"><span class="id" title="lemma">size_orbit</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.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="looping_order"><span class="id" title="lemma">looping_order</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.html#looping"><span class="id" title="definition">looping</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_orbit"><span class="id" title="lemma">fconnect_orbit</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="orbit_uniq"><span class="id" title="lemma">orbit_uniq</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="findex_max"><span class="id" title="lemma">findex_max</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#findex"><span class="id" title="definition">findex</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="findex_iter"><span class="id" title="lemma">findex_iter</span></a> <span class="id" title="var">x</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#findex"><span class="id" title="definition">findex</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</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.fingraph.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#i"><span class="id" title="variable">i</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_findex"><span class="id" title="lemma">iter_findex</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#findex"><span class="id" title="definition">findex</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="findex0"><span class="id" title="lemma">findex0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#findex"><span class="id" title="definition">findex</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_invariant"><span class="id" title="lemma">fconnect_invariant</span></a> (<span class="id" title="var">T'</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.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.fingraph.html#T'"><span class="id" title="variable">T'</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#invariant"><span class="id" title="definition">invariant</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#k"><span class="id" title="variable">k</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#xpredT"><span class="id" title="abbreviation">xpredT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Orbit.Loop"><span class="id" title="section">Loop</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Orbit.Loop.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="Orbit.Loop.f_p"><span class="id" title="variable">f_p</span></a> : <a class="idref" href="mathcomp.ssreflect.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a>) (<a name="Orbit.Loop.Up"><span class="id" title="variable">Up</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a>).<br/> +<span class="id" title="keyword">Variable</span> <a name="Orbit.Loop.x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Orbit.Loop.p_x"><span class="id" title="variable">p_x</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.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.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This lemma does not depend on Up : (uniq p) +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_cycle"><span class="id" title="lemma">fconnect_cycle</span></a> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="order_cycle"><span class="id" title="lemma">order_cycle</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.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.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="orbit_rot_cycle"><span class="id" title="lemma">orbit_rot_cycle</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><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#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</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 class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.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.seq.html#rot"><span class="id" title="definition">rot</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop"><span class="id" title="section">Loop</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Orbit.orbit_in"><span class="id" title="section">orbit_in</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Orbit.orbit_in.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_sort"><span class="id" title="projection">pred_sort</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predPredType"><span class="id" title="definition">predPredType</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Orbit.orbit_in.f_in"><span class="id" title="variable">f_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Orbit.orbit_in.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_in"><span class="id" title="lemma">iter_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_in"><span class="id" title="lemma">finv_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="f_finv_in"><span class="id" title="lemma">f_finv_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <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.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_f_in"><span class="id" title="lemma">finv_f_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <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.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_inj_in"><span class="id" title="lemma">finv_inj_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_sym_in"><span class="id" title="lemma">fconnect_sym_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_order_in"><span class="id" title="lemma">iter_order_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_finv_in"><span class="id" title="lemma">iter_finv_in</span></a> <span class="id" title="var">n</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="cycle_orbit_in"><span class="id" title="lemma">cycle_orbit_in</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, (<a class="idref" href="mathcomp.ssreflect.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fpath_finv_in"><span class="id" title="lemma">fpath_finv_in</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>))<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fpath_finv_f_in"><span class="id" title="lemma">fpath_finv_f_in</span></a> <span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/> + <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>))<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fpath_f_finv_in"><span class="id" title="lemma">fpath_f_finv_in</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.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><br/> + <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in"><span class="id" title="section">orbit_in</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Orbit.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="f_finv"><span class="id" title="lemma">f_finv</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.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_f"><span class="id" title="lemma">finv_f</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.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fin_inj_bij"><span class="id" title="lemma">fin_inj_bij</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#bijective"><span class="id" title="inductive">bijective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_bij"><span class="id" title="lemma">finv_bij</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#bijective"><span class="id" title="inductive">bijective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_inj"><span class="id" title="lemma">finv_inj</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fconnect_sym"><span class="id" title="lemma">fconnect_sym</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Orbit.symf"><span class="id" title="variable">symf</span></a> := <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect_sym"><span class="id" title="lemma">fconnect_sym</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_order"><span class="id" title="lemma">iter_order</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="iter_finv"><span class="id" title="lemma">iter_finv</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="cycle_orbit"><span class="id" title="lemma">cycle_orbit</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.path.html#fcycle"><span class="id" title="abbreviation">fcycle</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fpath_finv"><span class="id" title="lemma">fpath_finv</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#fpath"><span class="id" title="abbreviation">fpath</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#belast"><span class="id" title="definition">belast</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#p"><span class="id" title="variable">p</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_fconnect_finv"><span class="id" title="lemma">same_fconnect_finv</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fcard_finv"><span class="id" title="lemma">fcard_finv</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</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.fingraph.html#fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="order_set"><span class="id" title="definition">order_set</span></a> <span class="id" title="var">n</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.fingraph.html#Orbit.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#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.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.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fcard_order_set"><span class="id" title="lemma">fcard_order_set</span></a> <span class="id" title="var">n</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.fingraph.html#Orbit.T"><span class="id" title="variable">T</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order_set"><span class="id" title="definition">order_set</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fclosed"><span class="id" title="abbreviation">fclosed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard"><span class="id" title="abbreviation">fcard</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.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/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fclosed1"><span class="id" title="lemma">fclosed1</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.fingraph.html#Orbit.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fclosed"><span class="id" title="abbreviation">fclosed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="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.fingraph.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.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_fconnect1"><span class="id" title="lemma">same_fconnect1</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="same_fconnect1_r"><span class="id" title="lemma">same_fconnect1_r</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit"><span class="id" title="section">Orbit</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="FconnectId"><span class="id" title="section">FconnectId</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="FconnectId.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">Lemma</span> <a name="fconnect_id"><span class="id" title="lemma">fconnect_id</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#xpred1"><span class="id" title="abbreviation">xpred1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="order_id"><span class="id" title="lemma">order_id</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="orbit_id"><span class="id" title="lemma">orbit_id</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="froots_id"><span class="id" title="lemma">froots_id</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#froots"><span class="id" title="abbreviation">froots</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="froot_id"><span class="id" title="lemma">froot_id</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#froot"><span class="id" title="abbreviation">froot</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fcard_id"><span class="id" title="lemma">fcard_id</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.fingraph.html#FconnectId.T"><span class="id" title="variable">T</span></a>) : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard"><span class="id" title="abbreviation">fcard</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.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/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectId"><span class="id" title="section">FconnectId</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="FconnectEq"><span class="id" title="section">FconnectEq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="FconnectEq.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="FconnectEq.f"><span class="id" title="variable">f</span></a> <a name="FconnectEq.f'"><span class="id" title="variable">f'</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_eq_can"><span class="id" title="lemma">finv_eq_can</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.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="FconnectEq.eq_f"><span class="id" title="variable">eq_f</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> +<span class="id" title="keyword">Let</span> <a name="FconnectEq.eq_rf"><span class="id" title="variable">eq_rf</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#eq_frel"><span class="id" title="lemma">eq_frel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.eq_f"><span class="id" title="variable">eq_f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_fconnect"><span class="id" title="lemma">eq_fconnect</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#86efabaf3ab961ac3d2bac35d2b3c35d"><span class="id" title="notation">=2</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fconnect"><span class="id" title="abbreviation">fconnect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_fcard"><span class="id" title="lemma">eq_fcard</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#fcard_mem"><span class="id" title="abbreviation">fcard_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_finv"><span class="id" title="lemma">eq_finv</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_froot"><span class="id" title="lemma">eq_froot</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#froot"><span class="id" title="abbreviation">froot</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#froot"><span class="id" title="abbreviation">froot</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_froots"><span class="id" title="lemma">eq_froots</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#froots"><span class="id" title="abbreviation">froots</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#froots"><span class="id" title="abbreviation">froots</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq.f'"><span class="id" title="variable">f'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FconnectEq"><span class="id" title="section">FconnectEq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="FinvEq"><span class="id" title="section">FinvEq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="FinvEq.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="FinvEq.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="FinvEq.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="finv_inv"><span class="id" title="lemma">finv_inv</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="order_finv"><span class="id" title="lemma">order_finv</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order"><span class="id" title="definition">order</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="order_set_finv"><span class="id" title="lemma">order_set_finv</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#order_set"><span class="id" title="definition">order_set</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.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.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#order_set"><span class="id" title="definition">order_set</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n"><span class="id" title="variable">n</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#FinvEq"><span class="id" title="section">FinvEq</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="RelAdjunction"><span class="id" title="section">RelAdjunction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="RelAdjunction.T"><span class="id" title="variable">T</span></a> <a name="RelAdjunction.T'"><span class="id" title="variable">T'</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="RelAdjunction.h"><span class="id" title="variable">h</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#T'"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>) (<a name="RelAdjunction.e"><span class="id" title="variable">e</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T"><span class="id" title="variable">T</span></a>) (<a name="RelAdjunction.e'"><span class="id" title="variable">e'</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#T'"><span class="id" title="variable">T'</span></a>).<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="RelAdjunction.sym_e"><span class="id" title="variable">sym_e</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a>) (<a name="RelAdjunction.sym_e'"><span class="id" title="variable">sym_e'</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect_sym"><span class="id" title="definition">connect_sym</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Record</span> <a name="rel_adjunction_mem"><span class="id" title="record">rel_adjunction_mem</span></a> <span class="id" title="var">m_a</span> := <a name="RelAdjunction"><span class="id" title="constructor">RelAdjunction</span></a> {<br/> + <a name="rel_unit"><span class="id" title="projection">rel_unit</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#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</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#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">x'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.T'"><span class="id" title="variable">T'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.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.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>;<br/> + <a name="rel_functor"><span class="id" title="projection">rel_functor</span></a> <span class="id" title="var">x'</span> <span class="id" title="var">y'</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#m_a"><span class="id" title="variable">m_a</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.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y'"><span class="id" title="variable">y'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y'"><span class="id" title="variable">y'</span></a>)<br/> +}.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="RelAdjunction.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.fingraph.html#RelAdjunction.T"><span class="id" title="variable">T</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="RelAdjunction.cl_a"><span class="id" title="variable">cl_a</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.a"><span class="id" title="variable">a</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="intro_adjunction"><span class="id" title="lemma">intro_adjunction</span></a> (<span class="id" title="var">h'</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.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.fingraph.html#RelAdjunction.a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.T'"><span class="id" title="variable">T'</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">a_x</span>,<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#h'"><span class="id" title="variable">h'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a_x"><span class="id" title="variable">a_x</span></a>))<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span> <span class="id" title="var">a_y</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#h'"><span class="id" title="variable">h'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a_x"><span class="id" title="variable">a_x</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#h'"><span class="id" title="variable">h'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a_y"><span class="id" title="variable">a_y</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x'</span> <span class="id" title="var">a_x</span>,<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#h'"><span class="id" title="variable">h'</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a>) <a class="idref" href="mathcomp.ssreflect.fingraph.html#a_x"><span class="id" title="variable">a_x</span></a>)<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y'</span>, <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y'"><span class="id" title="variable">y'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#connect"><span class="id" title="definition">connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#x'"><span class="id" title="variable">x'</span></a>) (<a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#y'"><span class="id" title="variable">y'</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="strict_adjunction"><span class="id" title="lemma">strict_adjunction</span></a> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</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.fingraph.html#RelAdjunction.a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#rel_base"><span class="id" title="definition">rel_base</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">predC</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.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#c2f58fba484177bda65c2ab1289a6fe6"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="RelAdjunction.ccl_a"><span class="id" title="variable">ccl_a</span></a> := <a class="idref" href="mathcomp.ssreflect.fingraph.html#closed_connect"><span class="id" title="lemma">closed_connect</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.cl_a"><span class="id" title="variable">cl_a</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="adjunction_closed"><span class="id" title="lemma">adjunction_closed</span></a> : <a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</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.fingraph.html#closed"><span class="id" title="abbreviation">closed</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">preim</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.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#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="adjunction_n_comp"><span class="id" title="lemma">adjunction_n_comp</span></a> :<br/> + <a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</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.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e"><span class="id" title="variable">e</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#n_comp"><span class="id" title="abbreviation">n_comp</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.e'"><span class="id" title="variable">e'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">preim</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.h"><span class="id" title="variable">h</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.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#3270414d0a8e3a8c7d7f93021a19fb70"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction"><span class="id" title="section">RelAdjunction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</span></a> <span class="id" title="var">h</span> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction_mem"><span class="id" title="record">rel_adjunction_mem</span></a> <span class="id" title="var">h</span> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">a</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="a137391017d2b2508b7a048304776dea"><span class="id" title="notation">"</span></a>@ 'rel_adjunction' T T' h e e' a" :=<br/> + (@<a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction_mem"><span class="id" title="record">rel_adjunction_mem</span></a> <span class="id" title="var">T</span> <span class="id" title="var">T'</span> <span class="id" title="var">h</span> <span class="id" title="var">e</span> <span class="id" title="var">e'</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">a</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 10, <span class="id" title="var">T</span>, <span class="id" title="var">T'</span>, <span class="id" title="var">h</span>, <span class="id" title="var">e</span>, <span class="id" title="var">e'</span>, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="fun_adjunction"><span class="id" title="abbreviation">fun_adjunction</span></a> <span class="id" title="var">h</span> <span class="id" title="var">f</span> <span class="id" title="var">f'</span> <span class="id" title="var">a</span> := (<a class="idref" href="mathcomp.ssreflect.fingraph.html#rel_adjunction"><span class="id" title="abbreviation">rel_adjunction</span></a> <span class="id" title="var">h</span> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <span class="id" title="var">f</span>) (<a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <span class="id" title="var">f'</span>) <span class="id" title="var">a</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="339ad71b2d989ba85782b4c39218de1c"><span class="id" title="notation">"</span></a>@ 'fun_adjunction' T T' h f f' a" :=<br/> + (<a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">@</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">rel_adjunction</span></a> <span class="id" title="var">T</span> <span class="id" title="var">T'</span> <span class="id" title="var">h</span> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <span class="id" title="var">f</span><a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#frel"><span class="id" title="definition">frel</span></a> <span class="id" title="var">f'</span><a class="idref" href="mathcomp.ssreflect.fingraph.html#a137391017d2b2508b7a048304776dea"><span class="id" title="notation">)</span></a> <span class="id" title="var">a</span>)<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 10, <span class="id" title="var">T</span>, <span class="id" title="var">T'</span>, <span class="id" title="var">h</span>, <span class="id" title="var">f</span>, <span class="id" title="var">f'</span>, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">type_scope</span>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Unset Implicit Arguments</span>.<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 |