proposition: Lemma card_del_edge : num_edges del_edge < num_edges G.
proof: Proof. apply: proper_card. apply/properP; split. - apply/subrelP. exact: subrel_del_edge. - exists (a,b); by rewrite !inE //= /edge_rel /= !eqxx. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)