Return of PR #226: adds relevant theorems when fcycle f (orbit f x) and the needed lemmas (#261)

* adds relevant theorems when fcycle f (orbit f x) and the needed lemmas

* Generalize f_step lemmas

* Generalizations, shorter proofs, bugfixes, CHANGELOG

- changelog, renamings and comments
- renaming `homo_cycle` to `mem_fcycle` and other small renamings
- name swap `mem_orbit` and `in_orbit`
- simplifications
- generalization following @pi8027's comment
- Getting rid of many uniquness condition in `fingraph.v`
- added cases to the equivalence `orbitPcycle`
- added `cycle_catC`

5 files changed, 390 insertions, 59 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2047211..045733d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -13,7 +13,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added a `void` notation for the `Empty_set` type of the standard library, the
   canonical injection `of_void` and its cancellation lemma `of_voidK`, and
   `eq`, `choice`, `count` and `fin` instances.
-  
+
 - Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below).
 
 - Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
@@ -30,6 +30,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`,
   `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`.
 
+- Added theorems `nth_rcons_default`, `undup_rcons`, `undup_cat` and
+  `undup_flatten_nseq` in `seq.v`
+
 - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
   `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`,
   `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`,
@@ -59,8 +62,6 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
        `edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and
        `modn_pred`.
 
-- Added `mem2E` in `path.v`.
-
 - Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`.
 
 - Added map/parametricity theorems about `path`, `sort`, and `sorted`:
@@ -68,6 +69,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`,
   `sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`.
 
+- Extracting lemma `fpathE` from `fpathP`, and shortening the proof of
+  the latter.
+
 - Added the theorem `perm_iota_sort` to express that the sorting of
   any sequence `s` is equal to a mapping of `iota 0 (size s)` to the
   nth elements of `s`, so that one can still reason on `nat`, even
@@ -78,8 +82,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`,
   `sorted_subseq_sort`, and `mem2_sort`.
 
-- New algebraic interfaces : comAlgebra and comUnitAlgebra for
-  commutative and commutative-unitary algebras.
+- New algebraic interfaces in `ssralg.v`: comAlgebra and
+  comUnitAlgebra for commutative and commutative-unitary algebras.
 
 - Initial property for polynomials in algebras:
   New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element
@@ -95,19 +99,45 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Added ssrfun theorem `inj_compr`.
 
+- Added theorems `mem2E`, `nextE`, `mem_fcycle`, `inj_cycle`,
+  `take_traject`, `trajectD` and `cycle_catC` in `path.v`
+
+- Added lemmas about `cycle`, `connect`, `fconnect`, `order` and
+  `orbit` in `fingraph.v`:
+  - lemma `connect_cycle`,
+  - lemmas `in_orbit`, `order_gt0`, `findex_eq0`, `mem_orbit`,
+    `image_orbit`,
+  - lemmas `fcycle_rconsE`, `fcycle_consE`, `fcycle_consEflatten` and
+    `undup_cycle_cons` which operate under the precondition that the
+    sequence `x :: p` is a cycle for f (i.e. `fcycle f (x :: p)`).
+  - lemmas which operate under the precondition there is a sequence
+    `p` which is a cycle for `f` (i.e. `fcycle f p`):
+    `order_le_cycle`, `finv_cycle`, `f_finv_cycle`, `finv_f_cycle`,
+    `finv_inj_cycle`, `iter_finv_cycle`, `cycle_orbit_cycle`,
+    `fpath_finv_cycle`, `fpath_finv_f_cycle`, `fpath_f_finv_cycle`,
+    `prevE`, `fcycleEflatten`, `fcycle_undup`, `in_orbit_cycle`,
+    `eq_order_cycle`, `iter_order_cycle`,
+  - lemmas `injectivePcycle`, `orbitPcycle`, `fconnect_eqVf`,
+    `order_id_cycle`, `orderPcycle`, `fconnect_f`, `fconnect_findex`.
+
+- Added lemma `rot_index` which explicits the index given by `rot_to`.
+
+- Added tactic `tfae` to split an equivalence between n+1 propositions
+  into n+1 goals, and referenced orbitPcycle as a reference of use.
+
 ### Changed
 
 - Replaced the legacy generalised induction idiom with a more robust one
 that does not rely on the `{-2}` numerical occurrence selector, using
 new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`,  ...., (see above). The new idiom is documented in `ssrnat`.
    This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release (see [PR #434](https://github.com/math-comp/math-comp/pull/434) for examples).
-   
- - Replaced the use of the accidental convertibility between `enum A` and 
+
+ - Replaced the use of the accidental convertibility between `enum A` and
    `filter A (index_enum T)` with more explicit lemmas `big_enumP`, `big_enum`, `big_enum_cond`, `big_image` added to the `bigop` library, and deprecated the `filter_index_enum` lemma that states the corresponding equality. Both convertibility and equality may no longer hold in future `mathcomp` releases when sets over `finType`s are generalised to finite sets over `choiceType`s, so client libraries should stop relying on this identity. File `bigop.v` has some boilerplate to help with the port; also see [PR #441](https://github.com/math-comp/math-comp/pull/441) for examples.
-   
+
  - Restricted `big_image`, `big_image_cond`, `big_image_id` and `big_image_cond_id`
  to `bigop`s over _abelian_ monoids, anticipating the change in the definition of `enum`. This may introduce some incompatibilities - non-abelian instances should be dealt with a combination of `big_map` and `big_enumP`.
-   
+
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
   `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs
   simultaneous replacement of expressions of the form `x == y` and `y == x`
@@ -135,6 +165,10 @@ new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`,  ...., (see above). The
     `ssrnat.mc_1_9` module. One may compile proofs compatible with the version
     1.9 in newer versions by using this module.
 
+- Moved `iter_in` to ssrnat and reordered its arguments.
+
+- Notation `[<-> P0 ; .. ; Pn]` now forces `Pi` to be of type `Prop`.
+
 ### Removed
 
 - `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 671bb95..afd43df 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -166,6 +166,14 @@ move=> e_p y p_y; case/splitPl: p / p_y e_p => p q <-.
 by rewrite cat_path => /andP[e_p _]; apply/connectP; exists p.
 Qed.
 
+Lemma connect_cycle p : cycle e p -> {in p &, forall x y, connect x y}.
+Proof.
+move=> e_p x y /rot_to[i q rip]; rewrite -(mem_rot i) rip => yqx.
+have /= : cycle e (x :: q) by rewrite -rip rot_cycle.
+case/splitPl: yqx => r s lxr; rewrite rcons_cat cat_path => /andP[xr _].
+by apply/connectP; exists r.
+Qed.
+
 Definition root x := odflt x (pick (connect x)).
 
 Definition roots : pred T := fun x => root x == x.
@@ -395,6 +403,12 @@ apply/idP/idP=> [/connectP[_ /fpathP[m ->] ->] | /trajectP[i _ ->]].
 exact: fconnect_iter.
 Qed.
 
+Lemma in_orbit x : x \in orbit x. Proof. by rewrite -fconnect_orbit. Qed.
+Hint Resolve in_orbit : core.
+
+Lemma order_gt0 x : order x > 0. Proof. by rewrite -orderSpred. Qed.
+Hint Resolve order_gt0 : core.
+
 Lemma orbit_uniq x : uniq (orbit x).
 Proof.
 rewrite /orbit -orderSpred looping_uniq; set n := (order x).-1.
@@ -425,6 +439,12 @@ Qed.
 Lemma findex0 x : findex x x = 0.
 Proof. by rewrite /findex /orbit -orderSpred /= eqxx. Qed.
 
+Lemma findex_eq0 x y : (findex x y == 0) = (x == y).
+Proof.
+apply/idP/idP; last by move=> /eqP ->; rewrite findex0.
+by rewrite /findex /orbit -orderSpred /=; case: (x == y).
+Qed.
+
 Lemma fconnect_invariant (T' : eqType) (k : T -> T') :
   invariant f k =1 xpredT -> forall x y, fconnect f x y -> k x = k y.
 Proof.
@@ -432,56 +452,32 @@ move=> eq_k_f x y /iter_findex <-; elim: {y}(findex x y) => //= n ->.
 by rewrite (eqP (eq_k_f _)).
 Qed.
 
-Section Loop.
-
-Variable p : seq T.
-Hypotheses (f_p : fcycle f p) (Up : uniq p).
-Variable x : T.
-Hypothesis p_x : x \in p.
-
-(* This lemma does not depend on Up : (uniq p) *)
-Lemma fconnect_cycle y : fconnect f x y = (y \in p).
+Lemma mem_orbit x : {homo f : y / y \in orbit x}.
 Proof.
-have [i q def_p] := rot_to p_x; rewrite -(mem_rot i p) def_p.
-have{i def_p} /andP[/eqP q_x f_q]: (f (last x q) == x) && fpath f x q.
-  by have:= f_p; rewrite -(rot_cycle i) def_p (cycle_path x).
-apply/idP/idP=> [/connectP[_ /fpathP[j ->] ->] | ]; last exact: path_connect.
-case/fpathP: f_q q_x => n ->; rewrite !last_traject -iterS => def_x.
-by apply: (@loopingP _ f x n.+1); rewrite /looping def_x /= mem_head.
+by move=> y; rewrite -!fconnect_orbit => /connect_trans->//; apply: fconnect1.
 Qed.
 
-Lemma order_cycle : order x = size p.
-Proof. by rewrite -(card_uniqP Up); apply (eq_card fconnect_cycle). Qed.
-
-Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
+Lemma image_orbit x : {subset image f (orbit x) <= orbit x}.
 Proof.
-have [i q def_p] := rot_to p_x; exists i.
-rewrite /orbit order_cycle -(size_rot i) def_p.
-suffices /fpathP[j ->]: fpath f x q by rewrite /= size_traject.
-by move: f_p; rewrite -(rot_cycle i) def_p (cycle_path x); case/andP.
+by move=> _ /mapP[y yin ->]; apply: mem_orbit; rewrite ?mem_enum in yin.
 Qed.
 
-End Loop.
-
 Section orbit_in.
 
 Variable S : {pred T}.
 
-Hypothesis f_in : {in S, forall x, f x \in S}.
+Hypothesis f_in : {homo f : x / x \in S}.
 Hypothesis injf : {in S &, injective f}.
 
-Lemma iter_in : {in S, forall x i, iter i f x \in S}.
-Proof. by move=> x xS; elim=> [|i /f_in]. Qed.
-
-Lemma finv_in : {in S, forall x, finv x \in S}.
-Proof. by move=> ??; rewrite iter_in. Qed.
+Lemma finv_in : {homo finv : x / x \in S}.
+Proof. by move=> x xS; rewrite iter_in. Qed.
 
 Lemma f_finv_in : {in S, cancel finv f}.
 Proof.
 move=> x xS; move: (looping_order x) (orbit_uniq x).
 rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1.
 case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr.
-by move=> /injf ->; rewrite ?iter_in //; case/trajectP; exists i.
+by move=> /injf ->; rewrite ?(iter_in _ f_in) //; case/trajectP; exists i.
 Qed.
 
 Lemma finv_f_in : {in S, cancel f finv}.
@@ -516,8 +512,9 @@ move=> x xS; rewrite /orbit -orderSpred (cycle_path x) /= last_traject.
 by rewrite -/(finv x) fpath_traject f_finv_in ?eqxx.
 Qed.
 
-Lemma fpath_finv_in p x : (x \in S) && (fpath finv x p) =
-                          (last x p \in S) && (fpath f (last x p) (rev (belast x p))).
+Lemma fpath_finv_in p x :
+  (x \in S) && (fpath finv x p) =
+    (last x p \in S) && (fpath f (last x p) (rev (belast x p))).
 Proof.
 elim: p x => //= y p IHp x; rewrite rev_cons rcons_path.
 transitivity [&& y \in S, f y == x & fpath finv y p].
@@ -537,6 +534,15 @@ Proof. by move=> lS /(conj lS)/andP; rewrite -fpath_finv_in => /andP[]. Qed.
 
 End orbit_in.
 
+Lemma injectivePcycle x :
+  reflect {in orbit x &, injective f} (fcycle f (orbit x)).
+Proof.
+apply: (iffP idP) => [/inj_cycle//|/cycle_orbit_in].
+by apply; [apply: mem_orbit|apply: in_orbit].
+Qed.
+
+Section orbit_inj.
+
 Hypothesis injf : injective f.
 
 Lemma f_finv : cancel finv f. Proof. exact: (in1T (f_finv_in _ (in2W _))). Qed.
@@ -605,9 +611,230 @@ Proof. by apply: same_connect1 => /=. Qed.
 Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y).
 Proof. by apply: same_connect1r x => /=. Qed.
 
+End orbit_inj.
+Hint Resolve orbit_uniq : core.
+
+Section fcycle_p.
+Variables (p : seq T) (f_p : fcycle f p).
+
+Section mem_cycle.
+
+Variable (Up : uniq p) (x : T) (p_x : x \in p).
+
+(* fconnect_cycle does not dependent on Up *)
+Lemma fconnect_cycle y : fconnect f x y = (y \in p).
+Proof.
+have [i q def_p] := rot_to p_x; rewrite -(mem_rot i p) def_p.
+have{i def_p} /andP[/eqP q_x f_q]: (f (last x q) == x) && fpath f x q.
+  by have:= f_p; rewrite -(rot_cycle i) def_p (cycle_path x).
+apply/idP/idP=> [/connectP[_ /fpathP[j ->] ->] | ]; last exact: path_connect.
+case/fpathP: f_q q_x => n ->; rewrite !last_traject -iterS => def_x.
+by apply: (@loopingP _ f x n.+1); rewrite /looping def_x /= mem_head.
+Qed.
+
+(* order_le_cycle does not dependent on Up *)
+Lemma order_le_cycle : order x <= size p.
+Proof.
+apply: leq_trans (card_size _); apply/subset_leq_card/subsetP=> y.
+by rewrite !(fconnect_cycle, inE) ?eqxx.
+Qed.
+
+Lemma order_cycle : order x = size p.
+Proof. by rewrite -(card_uniqP Up); apply: (eq_card fconnect_cycle). Qed.
+
+Lemma orbitE : orbit x = rot (index x p) p.
+Proof.
+set i := index _ _; rewrite /orbit order_cycle -(size_rot i) rot_index// -/i.
+set q := _ ++ _; suffices /fpathP[j ->]: fpath f x q by rewrite /= size_traject.
+by move: f_p; rewrite -(rot_cycle i) rot_index// (cycle_path x); case/andP.
+Qed.
+
+Lemma orbit_rot_cycle : {i : nat | orbit x = rot i p}.
+Proof. by rewrite orbitE; exists (index x p). Qed.
+
+End mem_cycle.
+
+Let f_inj := inj_cycle f_p.
+Let homo_f := mem_fcycle f_p.
+
+Lemma finv_cycle : {homo finv : x / x \in p}. Proof. exact: finv_in. Qed.
+
+Lemma f_finv_cycle : {in p, cancel finv f}. Proof. exact: f_finv_in. Qed.
+
+Lemma finv_f_cycle : {in p, cancel f finv}. Proof. exact: finv_f_in. Qed.
+
+Lemma finv_inj_cycle : {in p &, injective finv}. Proof. exact: finv_inj_in. Qed.
+
+Lemma iter_finv_cycle n :
+  {in p, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
+Proof. exact: iter_finv_in. Qed.
+
+Lemma cycle_orbit_cycle : {in p, forall x, fcycle f (orbit x)}.
+Proof. exact: cycle_orbit_in. Qed.
+
+Lemma fpath_finv_cycle q x : (x \in p) && (fpath finv x q) =
+  (last x q \in p) && fpath f (last x q) (rev (belast x q)).
+Proof. exact: fpath_finv_in. Qed.
+
+Lemma fpath_finv_f_cycle q : {in p, forall x,
+  fpath finv x q -> fpath f (last x q) (rev (belast x q))}.
+Proof. exact: fpath_finv_f_in. Qed.
+
+Lemma fpath_f_finv_cycle q x : last x q \in p ->
+  fpath f (last x q) (rev (belast x q)) -> fpath finv x q.
+Proof. exact: fpath_f_finv_in. Qed.
+
+Lemma prevE x : x \in p -> prev p x = finv x.
+Proof.
+move=> x_p; have /eqP/(congr1 finv) := prev_cycle f_p x_p.
+by rewrite finv_f_cycle// mem_prev.
+Qed.
+
+End fcycle_p.
+
+Section fcycle_cons.
+Variables (x : T) (p : seq T) (f_p : fcycle f (x :: p)).
+
+Lemma fcycle_rconsE : rcons (x :: p) x = traject f x (size p).+2.
+Proof. by rewrite rcons_cons; have /fpathE-> := f_p; rewrite size_rcons. Qed.
+
+Lemma fcycle_consE : x :: p = traject f x (size p).+1.
+Proof. by have := fcycle_rconsE; rewrite trajectSr => /rcons_inj[/= <-]. Qed.
+
+Lemma fcycle_consEflatten : exists k, x :: p = flatten (nseq k.+1 (orbit x)).
+Proof.
+move: f_p; rewrite fcycle_consE; elim/ltn_ind: (size p) => n IHn t_cycle.
+have := order_le_cycle t_cycle (mem_head _ _); rewrite size_traject.
+case: ltngtP => //; last by move<-; exists 0; rewrite /= cats0.
+rewrite ltnS => n_ge _; have := t_cycle.
+rewrite -(subnKC n_ge) -addnS trajectD.
+rewrite (iter_order_in (mem_fcycle f_p) (inj_cycle f_p)) ?mem_head//.
+set m := (_ - _) => cycle_cat.
+have [||k->] := IHn m; last by exists k.+1.
+  by rewrite ltn_subrL (leq_trans _ n_ge) ?order_gt0.
+move: cycle_cat; rewrite -orderSpred/= rcons_cat rcons_cons -cat_rcons.
+by rewrite cat_path last_rcons => /andP[].
+Qed.
+
+Lemma undup_cycle_cons : undup (x :: p) = orbit x.
+Proof.
+by have [n {1}->] := fcycle_consEflatten; rewrite undup_flatten_nseq ?undup_id.
+Qed.
+
+End fcycle_cons.
+
+Section fcycle_undup.
+
+Variable (p : seq T) (f_p : fcycle f p).
+
+Lemma fcycleEflatten : exists k, p = flatten (nseq k (undup p)).
+Proof.
+case: p f_p => [//|x q] f_q; first by exists 0.
+have [k {1}->] := @fcycle_consEflatten x q f_q.
+by exists k.+1; rewrite undup_cycle_cons.
+Qed.
+
+Lemma fcycle_undup : fcycle f (undup p).
+Proof.
+case: p f_p => [//|x q] f_q; rewrite undup_cycle_cons//.
+by rewrite (cycle_orbit_in (mem_fcycle f_q) (inj_cycle f_q)) ?mem_head.
+Qed.
+
+Let p_undup_uniq := undup_uniq p.
+Let f_inj := inj_cycle f_p.
+Let homo_f := mem_fcycle f_p.
+
+Lemma in_orbit_cycle : {in p &, forall x, orbit x =i p}.
+Proof.
+by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup.
+Qed.
+
+Lemma eq_order_cycle : {in p &, forall x y, order y = order x}.
+Proof.
+by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup.
+Qed.
+
+Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.
+Proof.
+by move=> x y xp yp; rewrite (eq_order_cycle yp) ?(iter_order_in homo_f f_inj).
+Qed.
+
+End fcycle_undup.
+
+Section fconnect.
+
+Lemma fconnect_eqVf x y : fconnect f x y = (x == y) || fconnect f (f x) y.
+Proof.
+apply/idP/idP => [/iter_findex <-|/predU1P [<-|] //]; last first.
+  exact/connect_trans/fconnect1.
+by case: findex => [|i]; rewrite ?eqxx// iterSr fconnect_iter orbT.
+Qed.
+
+(*****************************************************************************)
+(* Lemma orbitPcycle is of type "The Following Are Equivalent", which means  *)
+(* all four statements are equivalent to each other. In order to use it, one *)
+(* has to apply it to the natural numbers corresponding to the line, e.g.    *)
+(* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`.   *)
+(* examples of this are in order_id_cycle and fconnnect_f.                   *)
+(* One may also use lemma all_iffLR to get a one sided impliciation, as in   *)
+(* orderPcycle.                                                              *)
+(*****************************************************************************)
+Lemma orbitPcycle {x} : [<->
+  (* 0 *) fcycle f (orbit x);
+  (* 1 *) order (f x) = order x;
+  (* 2 *) x \in fconnect f (f x);
+  (* 3 *) exists k, iter k.+1 f x = x;
+  (* 4 *) iter (order x) f x = x;
+  (* 5 *) {in orbit x &, injective f}].
+Proof.
+tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//].
+- by apply: eq_order_cycle xorbit_cycle _ _ _ _; rewrite ?mem_orbit.
+- move=> /subset_cardP/(_ _)->; rewrite ?inE//; apply/subsetP=> y.
+  by apply: connect_trans; apply: fconnect1.
+- by exists (findex (f x) x); rewrite // iterSr iter_findex.
+- apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//.
+  by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx.
+- rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-.
+  move=> /(congr1 (iter (order x).-1 f)); rewrite  -!iterSr !orderSpred.
+  by rewrite -!iter_add ![order _ + _]addnC !iter_add fx.
+Qed.
+
+Lemma order_id_cycle x : fcycle f (orbit x) -> order (f x) = order x.
+Proof. by move/(orbitPcycle 0 1). Qed.
+
+Inductive order_spec_cycle x : bool -> Type :=
+| OrderStepCycle of fcycle f (orbit x) & order x = order (f x) :
+    order_spec_cycle x true
+| OrderStepNoCycle of ~~ fcycle f (orbit x) & order x = (order (f x)).+1 :
+    order_spec_cycle x false.
+
+Lemma orderPcycle x : order_spec_cycle x (fcycle f (orbit x)).
+Proof.
+have [xcycle|Ncycle] := boolP (fcycle f (orbit x)); constructor => //.
+  by rewrite order_id_cycle.
+rewrite /order (eq_card (_ : _ =1 [predU1 x & fconnect f (f x)])).
+  by rewrite cardU1 inE (contraNN (all_iffLR orbitPcycle 2 0)).
+by move=> y; rewrite !inE fconnect_eqVf eq_sym.
+Qed.
+
+Lemma fconnect_f x : fconnect f (f x) x = fcycle f (orbit x).
+Proof. by apply/idP/idP => /(orbitPcycle 0 2). Qed.
+
+Lemma fconnect_findex x y :
+  fconnect f x y -> y != x -> findex x y = (findex (f x) y).+1.
+Proof.
+rewrite /findex fconnect_orbit /orbit -orderSpred /= inE => /orP [-> //|].
+rewrite eq_sym; move=> yin /negPf->; have [_ eq_o|_ ->//] := orderPcycle x.
+by rewrite -(orderSpred (f x)) trajectSr -cats1 index_cat -eq_o yin.
+Qed.
+
+End fconnect.
+
 End Orbit.
 
+Hint Resolve in_orbit mem_orbit order_gt0 orbit_uniq : core.
 Prenex Implicits order orbit findex finv order_set.
+Arguments orbitPcycle {T f x}.
 
 Section FconnectId.
 
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index abdf23b..d9ab11c 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -157,6 +157,10 @@ Qed.
 
 End Paths.
 
+Lemma cycle_catC (T : Type) (e : rel T) (p q : seq T) :
+  cycle e (p ++ q) = cycle e (q ++ p).
+Proof. by rewrite -rot_size_cat rot_cycle. Qed.
+
 Arguments pathP {T e x p}.
 
 Section HomoPath.
@@ -1010,6 +1014,13 @@ rewrite trajectSr nth_rcons size_traject.
 by case: ltngtP le_i_n => [? _||->] //; apply: IHn.
 Qed.
 
+Lemma trajectD m n x :
+  traject x (m + n) = traject x m ++ traject (iter m f x) n.
+Proof. by elim: m => //m IHm in x *; rewrite addSn !trajectS IHm -iterSr. Qed.
+
+Lemma take_traject n k x : k <= n -> take k (traject x n) = traject x k.
+Proof. by move=> /subnKC<-; rewrite trajectD take_size_cat ?size_traject. Qed.
+
 End Trajectory.
 
 Section EqTrajectory.
@@ -1022,13 +1033,13 @@ Proof. by move/eq_frel/eq_path. Qed.
 Lemma eq_fcycle f' : f =1 f' -> fcycle f =1 fcycle f'.
 Proof. by move/eq_frel/eq_cycle. Qed.
 
+Lemma fpathE x p : fpath f x p -> p = traject f (f x) (size p).
+Proof. by elim: p => //= y p IHp in x * => /andP[/eqP{y}<- /IHp<-]. Qed.
+
 Lemma fpathP x p : reflect (exists n, p = traject f (f x) n) (fpath f x p).
 Proof.
-elim: p x => [|y p IHp] x; first by left; exists 0.
-rewrite /= andbC; case: IHp => [fn_p | not_fn_p]; last first.
-  by right=> [] [[//|n]] [<- fn_p]; case: not_fn_p; exists n.
-apply: (iffP eqP) => [-> | [[] // _ []//]].
-by have [n ->] := fn_p; exists n.+1.
+apply: (iffP idP) => [/fpathE->|[n->]]; first by exists (size p).
+by elim: n => //= n IHn in x *; rewrite eqxx IHn.
 Qed.
 
 Lemma fpath_traject x n : fpath f x (traject f (f x) n).
@@ -1076,6 +1087,25 @@ Arguments loopingP {T f x n}.
 Arguments trajectP {T f x n y}.
 Prenex Implicits traject.
 
+Section Fcycle.
+Variables (T : eqType) (f : T -> T) (p : seq T) (f_p : fcycle f p).
+
+Lemma nextE (x : T) (p_x : x \in p) : next p x = f x.
+Proof. exact/esym/eqP/(next_cycle f_p). Qed.
+
+Lemma mem_fcycle : {homo f : x / x \in p}.
+Proof. by move=> x xp; rewrite -nextE// mem_next. Qed.
+
+Lemma inj_cycle : {in p &, injective f}.
+Proof.
+apply: can_in_inj (iter (size p).-1 f) _ => x /rot_to[i q rip].
+have /fpathE qxE : fcycle f (x :: q) by rewrite -rip rot_cycle.
+have -> : size p = size (rcons q x) by rewrite size_rcons -(size_rot i) rip.
+by rewrite -iterSr -last_traject prednK -?qxE ?size_rcons// last_rcons.
+Qed.
+
+End Fcycle.
+
 Section UniqCycle.
 
 Variables (n0 : nat) (T : eqType) (e : rel T) (p : seq T).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5566a44..0ddd382 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -180,12 +180,17 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 (*  if T : [<-> P0; P1; ..; Pn]  is such an equivalence, and i, j are in nat  *)
 (*  then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj;     *)
 (*  when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0.          *)
+(*  The tactic tfae splits the goal into n+1 implications to prove.           *)
+(*  An example of use can be found in fingraph theorem orbitPcycle.           *)
 (******************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Reserved Notation "[ '<->' P0 ; P1 ; .. ; Pn ]"
+  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]").
+
 Delimit Scope seq_scope with SEQ.
 Open Scope seq_scope.
 
@@ -384,6 +389,11 @@ Lemma nth_rcons s x n :
     if n < size s then nth s n else if n == size s then x else x0.
 Proof. by elim: s n => [|y s IHs] [] //=; apply: nth_nil. Qed.
 
+Lemma nth_rcons_default s i : nth (rcons s x0) i = nth s i.
+Proof.
+by rewrite nth_rcons; case: ltngtP => //[/ltnW ?|->]; rewrite nth_default.
+Qed.
+
 Lemma nth_ncons m x s n :
   nth (ncons m x s) n = if n < m then x else nth s (n - m).
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -1275,6 +1285,15 @@ Qed.
 Lemma undup_nil s : undup s = [::] -> s = [::].
 Proof. by case: s => //= x s; rewrite -mem_undup; case: ifP; case: undup. Qed.
 
+Lemma undup_cat s t :
+  undup (s ++ t) = [seq x <- undup s | x \notin t] ++ undup t.
+Proof. by elim: s => //= x s ->; rewrite mem_cat; do 2 case: in_mem => //=. Qed.
+
+Lemma undup_rcons s x : undup (rcons s x) = rcons [seq y <- undup s | y != x] x.
+Proof.
+by rewrite -!cats1 undup_cat; congr cat; apply: eq_filter => y; rewrite inE.
+Qed.
+
 (* Lookup *)
 
 Definition index x := find (pred1 x).
@@ -1336,16 +1355,24 @@ Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed.
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
 Proof. by apply: inj_eq; apply: rot_inj. Qed.
 
-Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+End EqSeq.
 
-Lemma rot_to s x : x \in s -> rot_to_spec s x.
+Section RotIndex.
+Variables (T : eqType).
+Implicit Types x y z : T.
+
+Lemma rot_index s x (i := index x s) : x \in s ->
+  rot i s = x :: (drop i.+1 s ++ take i s).
 Proof.
-move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s).
-rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs.
-by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0.
+by move=> x_s; rewrite /rot (drop_nth x) ?index_mem ?nth_index// cat_cons.
 Qed.
 
-End EqSeq.
+Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+
+Lemma rot_to s x : x \in s -> rot_to_spec s x.
+Proof. by move=> /rot_index /RotToSpec. Qed.
+
+End RotIndex.
 
 Definition inE := (mem_seq1, in_cons, inE).
 
@@ -2825,6 +2852,14 @@ Lemma flatten_map1 (S T : Type) (f : S -> T) s :
   flatten [seq [:: f x] | x <- s] = map f s.
 Proof. by elim: s => //= s0 s ->. Qed.
 
+Lemma undup_flatten_nseq n (T : eqType) (s : seq T) : 0 < n ->
+  undup (flatten (nseq n s)) = undup s.
+Proof.
+elim: n => [|[|n]/= IHn]//= _; rewrite ?cats0// undup_cat {}IHn//.
+rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => x.
+by rewrite mem_undup mem_cat => ->.
+Qed.
+
 Lemma sumn_flatten (ss : seq (seq nat)) :
   sumn (flatten ss) = sumn (map sumn ss).
 Proof. by elim: ss => // s ss /= <-; apply: sumn_cat. Qed.
@@ -3326,8 +3361,8 @@ Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
     if Qs is Q :: Qs then all_iff_and (P -> Q) (loop Q Qs) else P -> P0 in
   loop P0 Ps.
 
-Lemma all_iffLR P0 Ps :
-   all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
+Lemma all_iffLR P0 Ps : all_iff P0 Ps ->
+  forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
 Proof.
 move=> iffPs; have PsS n: nth P0 Ps n -> nth P0 Ps n.+1.
   elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case.
@@ -3352,9 +3387,10 @@ Arguments all_iffP {P0 Ps}.
 Coercion all_iffP : all_iff >-> Funclass.
 
 (* This means "the following are all equivalent: P0, ... Pn" *)
-Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
-  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
-  : form_scope.
+Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
+  (all_iff P0 (@cons Prop P1 (.. (@cons Prop Pn nil) ..))) : form_scope.
+
+Ltac tfae := do !apply: AllIffConj.
 
 (* Temporary backward compatibility. *)
 Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 9f826aa..b518c96 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -891,6 +891,7 @@ Section Iteration.
 Variable T : Type.
 Implicit Types m n : nat.
 Implicit Types x y : T.
+Implicit Types S : {pred T}.
 
 Definition iter n f x :=
   let fix loop m := if m is i.+1 then f (loop i) else x in loop n.
@@ -927,6 +928,9 @@ Proof. by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed.
 Lemma eq_iterop n op op' : op =2 op' -> iterop n op =2 iterop n op'.
 Proof. by move=> eq_op x; apply: eq_iteri; case. Qed.
 
+Lemma iter_in f S i : {homo f : x / x \in S} -> {homo iter i f : x / x \in S}.
+Proof. by move=> f_in x xS; elim: i => [|i /f_in]. Qed.
+
 End Iteration.
 
 Lemma iter_succn m n : iter n succn m = m + n.