proposition: Lemma add_edge_uforest': forall (g: PGraph) e' u v, uforest' g -> vvalid g u -> vvalid g v -> ~ connected g u v -> uforest' (pregraph_add_edge g e' u v).
proof: Proof. intros. assert (Huv: u<>v). unfold not; intros; subst u. pose proof (connected_refl g v H1). auto. split. intros. destruct (EE e e'). unfold Equivalence.equiv in e0. subst e. rewrite add_edge_src, add_edge_dst; simpl; auto. unfold RelationClasses.complement, Equivalence.equiv in c. apply add_edge_evalid_rev in H3. 2: auto. rewrite add_edge_preserves_src by auto. rewrite add_edge_preserves_dst by auto. apply H; auto. split. intros. destruct H3. destruct (prod_EV (u0,v0) (u,v)). hnf in e; inversion e. subst u0; subst v0. clear e. rewrite (add_edge_unique_adj_edge g e' u v e1); auto. rewrite (add_edge_unique_adj_edge g e' u v e2); auto. destruct (prod_EV (u0,v0) (v,u)). hnf in e; inversion e. subst u0 v0. clear e c. apply adj_edge_sym in H3. apply adj_edge_sym in H4. rewrite (add_edge_unique_adj_edge g e' u v e1); auto. rewrite (add_edge_unique_adj_edge g e' u v e2); auto. unfold complement, equiv in c, c0. apply add_edge_adj_edge2 in H3. apply add_edge_adj_edge2 in H4. destruct H. destruct H5. apply (H5 u0 v0). split; auto. unfold not; intros; subst e2. destruct H4. rewrite add_edge_src, add_edge_dst in H6. destruct H6; destruct H6; subst u0; subst v0; contradiction. unfold not; intros; subst e1. destruct H3. rewrite add_edge_src, add_edge_dst in H6. destruct H6; destruct H6; subst u0; subst v0; contradiction. split. intros. destruct (EE e e'). unfold Equivalence.equiv in e0. subst e. apply add_edge_strong_evalid; simpl; auto. unfold RelationClasses.complement, Equivalence.equiv in c. apply add_edge_preserves_strong_evalid. auto. apply add_edge_evalid_rev in H3; auto. apply H. auto. apply add_edge_unique_simple_upath; auto. apply H. 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