proposition: Lemma hom_comp F G H hv he hd kv ke kd : @is_hom F G hv he hd -> @is_hom G H kv ke kd -> is_hom (kv \o hv) (ke \o he) (fun e => hd e (+) kd (he e)).
proof: Proof. intros E E'. split. move=>e b=>/=; first by rewrite 2!endpoint_hom addbA. - move=>x/=. rewrite vlabel_hom (eqv_bigr _ (fun u _ => vlabel_hom (is_hom := E) u)). rewrite [X in _ ≡ X](partition_big _ (fun u => kv u == x)); last by move=>?;apply. apply: eqv_bigr => y /eqP <-. apply: eqv_big => // z. case e: (_ == y) => //. by rewrite (eqP e) eqxx. - move=>e/=. generalize (@elabel_hom _ _ _ _ _ E e). generalize (@elabel_hom _ _ _ _ _ E' (he e)). case (hd e); case (kd (he e)); simpl. + apply eqv11. + apply eqv01. + apply eqv10. + apply transitivity. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)