proposition: Lemma dhom_comp F G H h k: @is_dhom F G h -> @is_dhom G H k -> is_dhom (k \o h).
proof: Proof. intros E E' => x y O. apply E', E, O. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)