proposition: Lemma par_steps_r G G' H: steps G G' -> steps (H∥G) (H∥G').
proof: Proof. intro. rewrite parC. etransitivity. apply par_steps_l. eassumption. by rewrite parC. 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)