proposition: Lemma diso_card_edge (G H : sgraph) : diso G H -> #|E(G)| = #|E(H)|.
proof: Proof. case => -[g h can_g can_h] /= hom_g hom_h; apply/eqP. rewrite eqn_leq (sub_card_edge g) ?(sub_card_edge h) //; exact: can_inj. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)