proposition: Lemma dot_steps_l G G' H: steps G G' -> steps (G·H) (G'·H).
proof: Proof. apply: (step_to_steps (f:=fun G => G·H)) => {G G'}. - move => F G E. exact: dot_eqv. - move => G G' GG'. etransitivity. apply (@merge_step G') => //=. + rewrite /admissible_l/=. by rewrite !inE eqxx. + by rewrite /replace_ioL/= eqxx. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)