proposition: Lemma dot2unit_l (G: graph2) a: unit_graph2 a · G ≃2 G [tst input <- a].
proof: Proof. irewrite (iso2_sym (cnv2I _)). irewrite' (iso2_sym (cnv2I _)). apply cnv_iso2. irewrite cnv2dot. apply dot2unit_r. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)