proposition: Lemma cycle_all2rel (T : Type) (leT : rel T) : transitive leT -> forall s, cycle leT s = all2rel leT s.
proof: Proof. move=> leT_tr; elim=> //= x s IHs. rewrite allrel_cons2 -{}IHs // (path_sortedE leT_tr) /= all_rcons -rev_sorted. rewrite rev_rcons /= (path_sortedE (rev_trans leT_tr)) all_rev !andbA. case: (boolP (leT x x && _ && _)) => //=. case: s => //= y s /and3P[/and3P[_ xy _] yx sx]. rewrite rev_sorted rcons_path /= (leT_tr _ _ _ _ xy) ?andbT //. by case: (lastP s) sx => //= {}s z; rewrite all_rcons last_rcons => /andP [->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)