proposition: Lemma can_bijD1_fwd : cancel bijD1_fwd bijD1_bwd.
proof: Proof. move => [x|] //=; rewrite /bijD1_bwd; case: {-}_ /boolP => [|i] //. all: rewrite ?(negbTE (valP x)) ?valK' //. case:notF. by rewrite inE eqxx in i. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)