proposition: Lemma sub_in_cycle s : all P s -> cycle e s -> cycle e' s.
proof: Proof. case: s => //= x s /andP [Px Ps]. by apply: sub_in_path; rewrite /= all_rcons Px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)