proposition: Lemma uforest_no_multigraph: forall g (u v : V) (e1 e2 : E), uforest g -> adj_edge g e1 u v /\ adj_edge g e2 u v -> e1 = e2.
proof: Proof. intros. rename H0 into H1. destruct H. destruct H1. destruct (EE e1 e2). hnf in e; auto. unfold complement, equiv in c. exfalso. apply (H0 (u::v::u::nil) (e1::e2::nil)). split. simpl. apply NoDup_cons. unfold not; intros. destruct H3. 2: contradiction. subst v. destruct H2. apply (uforest_no_self_loops g e2); auto. split. apply H. apply H0. apply H2. destruct H3; destruct H3; subst u; auto. apply NoDup_cons. unfold not; intros; auto. apply NoDup_nil. unfold ucycle. split. unfold connected_by_path. simpl. split; auto. split. exists e1; auto. split. apply adjacent_symm. exists e1; auto. apply adj_edge_vvalid in H1. apply H1. split. simpl. split. auto. split. apply adj_edge_sym; auto. apply adj_edge_vvalid in H2; apply H2. apply NoDup_cons. unfold not; intros. destruct H3. symmetry in H3; contradiction. contradiction. apply NoDup_cons. unfold not; intros; auto. apply NoDup_nil. 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