proposition: Lemma gremove_is_componded_mark: forall root (g1 g2: Graph) e, out_edges g1 root e -> (marked g1) (dst g1 e) -> gremove_edge g1 e g2 -> (forall v : V, (marked g1) v <-> (marked g2) v) -> componded root (mark (dst g1 e)) g1 g2.
proof: Proof. intros. unfold componded. apply (compond_intro (compond_relation (nothing root) (mark (dst g1 e))) (nothing root) g1 g1 g2). + apply (compond_intro (nothing root) (mark (dst g1 e)) g1 g1 g1). - apply eq_do_nothing; auto. - split; intros. * reflexivity. * pose proof reachable_by_head_prop g1 (dst g1 e) n (unmarked g1). unfold unmarked at 2 in H3. rewrite negateP_spec in H3. tauto. + apply (gremove_is_nothing root g1 g2 e); 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