proposition: Lemma steps_of (G H : pre_graph) (isG : is_graph G) (isH : is_graph H) : osteps G H -> steps (pack G) (pack H).
proof: Proof. move => S. elim: S isG isH => {G H} [G H h|G H GH|G H GH|G F H S IH1 _ IH2] isG isH. - apply: iso_step. apply (eqvG_iso2L isG) in h. apply: iso2_comp (iso2_comp (oiso2_iso h) _); apply: pack_irrelevance. - destruct GH. apply iso_step. apply iso_of_oiso. apply add_edge_flip=>//. - exact: steps_of_ostep. - have isF : is_graph F by apply: osteps_graph S. by transitivity (pack F). Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)