proposition: Lemma sub_card_edge (G H : sgraph) (h : G -> H) : injective h -> is_dhom h -> #|E(G)| <= #|E(H)|.
proof: Proof. move=> inj_h hom_h ; pose h' (e : {set G}) := h @: e. have inj_h' : {in E(G) &, injective h'} by apply:in2W; apply: imset_inj. rewrite -(card_in_imset inj_h'); apply/subset_leq_card/subsetP => ?. case/imsetP => e /edgesP [x[y [-> /hom_h xy]]] ->; apply/edgesP; exists (h x),(h y). by rewrite /h' imsetU1 imset_set1. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)