proposition: Lemma can_bijD1_bwd : cancel bijD1_bwd bijD1_fwd.
proof: Proof. move => x. by rewrite /bijD1_bwd; case: {-}_ /boolP => [|i] //= /set1P->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)