proposition: Lemma gremove_is_nothing: forall root (g1 g2: Graph) e, out_edges g1 root e -> gremove_edge g1 e g2 -> (forall v : V, (marked g1) v <-> (marked g2) v) -> nothing root g1 g2.
proof: Proof. intros. split; auto. hnf. simpl. unfold predicate_vvalid. unfold predicate_weak_evalid. destruct H0 as [? [? [? [? ?]]]]. split; [|split;[|split]]; intros. + specialize (H0 v). intuition. + destruct_eq_dec e0 e. - subst. split; intros; destruct H6; unfold Complement in H7; unfold Ensembles.In in H7; destruct H; exfalso; auto. destruct H5; auto. destruct H5 as [_ [? _]]. apply H7. rewrite <- H5. auto. - specialize (H2 _ H6). specialize (H3 _ H6). split; intros; [rewrite <- H3 | rewrite H3]; intuition. + destruct H6, H7. rewrite H3; auto. intro. subst. unfold Complement in H8. unfold Ensembles.In in H8. destruct H; auto. + destruct H6, H7. rewrite H4; auto. intro. subst. unfold Complement in H8. unfold Ensembles.In in H8. destruct H; auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical