proposition: Lemma dot_steps_r G G' H: steps G G' -> steps (H·G) (H·G').
proof: Proof. move => GG'. rewrite dotcnv. transitivity ((G'°·H°)°). by apply cnv_steps, dot_steps_l, cnv_steps. by rewrite -dotcnv. 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)