proposition: Lemma cycle_min_intro : forall x l, cycle x l -> exists m, exists y, exists p, exists q, x :: l = m ++ y :: p ++ q /\ cycle_min y p.
proof: Proof. intros. unfold cycle_min. ded (nodup_intro eq_dec (x::l)). decomp H0. exists nil. exists x. exists l. exists nil. rewrite <- app_nil_end. simpl in H1. intuition. rewrite H1. ded (in_elim H4). decomp H0. rewrite H5. exists x3. exists x1. exists x4. exists (x1::x2). rewrite app_ass. simpl. rewrite H5 in H2. ded (nodup_app_elim H2). simpl in H0. decomp H0. intuition. destruct x0. contr. injection H1; intros. subst a. unfold cycle in H. destruct x3; injection H5; intros. subst x1. subst x4. rewrite H0 in H. ded (path_app_elim H). intuition. subst a. subst x0. rewrite app_ass in H0. simpl in H0. rewrite H0 in H. ded (path_app_elim H). destruct H7. ded (path_app_elim H10). intuition. Qed.
imports: Coq(Relations) CoLoR(LogicUtil Path ListUtil ListNodup)