proposition: Lemma uforest'_no_simple_ucycles: forall g, uforest' g -> (forall p l, valid_upath g p -> fits_upath g l p -> ~ simple_ucycle g p l).
proof: Proof. intros. destruct H as [Hself [Hmulti [Hstrong Hforest]]]. unfold not; intros. destruct H. destruct p. contradiction. destruct p. contradiction. destruct l. contradiction. destruct H2. destruct H2 as [_ [_ ?]]. destruct H3 as [_ ?]. simpl in H. apply NoDup_cons_2 in H3. assert (v <> v0). unfold not; intros. subst v0. destruct H1. destruct H1. destruct H1. apply Hself in H1. destruct H5; destruct H5; rewrite H5 in H1; rewrite H7 in H1; contradiction. destruct H1. assert (simple_upath g (v::v0::nil)). split. simpl; split. exists e; auto. apply (valid_upath_vvalid _ _ _ H0). right; left; auto. apply NoDup_cons. unfold not; intros; destruct H6. symmetry in H6; contradiction. contradiction. apply NoDup_cons. auto. apply NoDup_nil. assert (simple_upath g (v0::p)). split. apply valid_upath_tail in H0. simpl in H0; auto. auto. assert ((v::v0::nil) = (rev (v0::p))). apply (Hforest v v0). auto. split. apply H6. split; simpl; auto. apply simple_upath_rev; auto. apply connected_by_path_rev. split. apply H7. split. simpl; auto. rewrite last_error_cons in H2; auto. unfold not; intros. inversion H8. pose proof (fits_upath_rev g (v0::p) l H5). rewrite <- H8 in H9. destruct (rev l) eqn:Hrevl. contradiction. destruct l0. 2: simpl in H9; destruct H9; contradiction. simpl in H9. destruct H9 as [? _]. assert (e = e0). apply (Hmulti v v0). split; auto. subst e0. apply H3. apply in_rev. rewrite Hrevl. left; auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph