proposition: Lemma ucycle_induced (s : seq induced) : ucycle (--) s = ucycle (--) [seq val x | x <- s].
proof: Proof. rewrite /ucycle map_inj_uniq; last exact: val_inj; congr (_ && _). rewrite /cycle; case: s => //= x s. rewrite -map_rcons. by elim: (rcons s x) {1 3}x => //= {x s} y s <- x. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)