proposition: Lemma ihom_sym (F G: graph) (hv: bij F G) (he: bij (edge F) (edge G)) hd: is_ihom hv he hd -> is_ihom hv^-1 he^-1 (hd \o he^-1).
proof: Proof. intro H. split. - move=>e b=>/=. by rewrite -{3}(bijK' he e) endpoint_ihom bijK addbA addbb. - move=>x/=. by rewrite -{2}(bijK' hv x) vlabel_ihom. - move=>e/=. generalize (@elabel_ihom _ _ _ _ _ H (he^-1 e)). rewrite -{3}(bijK' he e) bijK'. by symmetry. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)