diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.fingraph.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.fingraph.html | 651 |
1 files changed, 0 insertions, 651 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.fingraph.html b/docs/htmldoc/mathcomp.ssreflect.fingraph.html deleted file mode 100644 index 6b8a8a5..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.fingraph.html +++ /dev/null @@ -1,651 +0,0 @@ -<!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/> - -<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 reflexive 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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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="mathcomp.ssreflect.ssrbool.html#fea9f4d81fed4d4bd9309c8e510110f0"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#407cde5b61fbf27196d1a7c5a475e083"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#1c170b7d9dd618ec64d5610e390a3afe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#1c170b7d9dd618ec64d5610e390a3afe"><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#407cde5b61fbf27196d1a7c5a475e083"><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#1c170b7d9dd618ec64d5610e390a3afe"><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#1c170b7d9dd618ec64d5610e390a3afe"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#dfs"><span class="id" title="definition">dfs</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#subpred"><span class="id" title="definition">subpred</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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#407cde5b61fbf27196d1a7c5a475e083"><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/V8.9.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/V8.9.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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.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/V8.9.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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#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#234f50e13366f794cd6877cf832a5935"><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/V8.9.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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><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/V8.9.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> : <span class="id" title="var">core</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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#EqConnect.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#0dacc1786c5ba797d47dd85006231633"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Closure.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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#f953bf7095e0da1cb644443fd0e17d6d"><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#f953bf7095e0da1cb644443fd0e17d6d"><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#f953bf7095e0da1cb644443fd0e17d6d"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">).-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#00fe0eaf5e6949f0a31725357afa4bba"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#xpredT"><span class="id" title="abbreviation">xpredT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.Loop.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">i</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">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.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#finv"><span class="id" title="definition">finv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#Orbit.orbit_in.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">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.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#ea2ff3d561159081cea6fb2e8113cc54"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">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.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) :<br/> - <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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><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#506674b18256ef8f50efed43fa1dfd7d"><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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">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.ssrbool.html#64f8873130736b599801d4930af00e74"><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="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#c717e24548d7d4d1086535addc681262"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">x'</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#RelAdjunction.a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#790b887fcb3f1d578b2c7a5460f7aeb5"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#83755aca2de7eb9ea173a9881e23c03e"><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/V8.9.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="0bca91535c00b0d2a53c08442a2249c5"><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/V8.9.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="e4a36380529526574f433f82cd2335d9"><span class="id" title="notation">"</span></a>@ 'fun_adjunction' T T' h f f' a" :=<br/> - (<a class="idref" href="mathcomp.ssreflect.fingraph.html#0bca91535c00b0d2a53c08442a2249c5"><span class="id" title="notation">@</span></a><a class="idref" href="mathcomp.ssreflect.fingraph.html#0bca91535c00b0d2a53c08442a2249c5"><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#0bca91535c00b0d2a53c08442a2249c5"><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#0bca91535c00b0d2a53c08442a2249c5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fingraph.html#0bca91535c00b0d2a53c08442a2249c5"><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#0bca91535c00b0d2a53c08442a2249c5"><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 |