proposition: Lemma connected_ufroot_same: forall (g: UFGraph) u v, connected g u v -> ufroot_same g u v.
proof: Proof. intros. rewrite connected_exists_path in H. destruct H as [p [? [? ?]]]. generalize dependent u. induction p. - intros. inversion H1. - destruct p. + intros. simpl in H1, H0. inversion H1. inversion H0. subst. apply (ufroot_same_refl _ (liGraph g)). simpl in H; trivial. + destruct H. rewrite last_error_cons in H1. 2: unfold not; inversion 1. specialize (IHp H0 H1). intros. simpl in H2. inversion H2; subst a; clear H2. apply adjacent_ufroot_same in H. apply (ufroot_same_trans _ (liGraph g) _ z); trivial. apply IHp. trivial. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.undirected_graph