fact: Definition bijD1_bwd (x : T) : option { x : T | x \notin [set z]} := if @boolP (x \in [set z]) is AltFalse p then Some (Sub x p) else None.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)