proposition: Lemma cycle_all2rel_in (T : Type) (P : {pred T}) (leT : rel T) : {in P & &, transitive leT} -> forall s, all P s -> cycle leT s = all2rel leT s.
proof: Proof. move=> /in3_sig leT_tr _ /all_sigP [s ->]. by rewrite cycle_map allrel_mapl allrel_mapr; apply: cycle_all2rel. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)