proposition: Lemma ostep_graph (F G : pre_graph) (isG : is_graph F) : ostep F G -> is_graph G.
proof: Proof. Proof with eauto with typeclass_instances. case => {G}... - move => x y z e1 e2 u v Iz D IOz xDz yDz arc_e1 arc_e2. apply: add_edge_graph'; rewrite /= in_fsetD1 ?xDz ?yDz /=. exact: oarc_vsetL arc_e1. exact: oarc_vsetR arc_e2. - move => x y e1 e2 u v e1De2 arc_e1 arc_e2. apply: add_edge_graph'. exact: oarc_vsetL arc_e1. exact: oarc_vsetR arc_e2. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)