proposition: Lemma osteps_iso (F G H: pre_graph): osteps F H -> F ⩭2 G -> exists U, osteps G U /\ inhabited (H ⩭2 U).
proof: Proof. intro S. revert G. induction S as [F G FG|F G FG|F G FG|F G H FG IH GH IH']; intros F' FF'. - exists F'. split. by []. exists. transitivity F=>//. symmetry. apply eqvG_iso2L=>//. apply FF'. - exists F'. split=>//. destruct FG. exists. etransitivity. 2: eassumption. symmetry. apply add_edge_flip=>//. apply FF'. - destruct (ostep_iso FG FF') as [U [F'U GU]]. exists U. split. by apply ostep_step. by exists. - destruct (IH _ FF') as [G' [F'G' [GG']]]. destruct (IH' _ GG') as [H' [G'H' [HH']]]. exists H'. split=>//. by transitivity G'. 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)