fact: Record bij (A B: Type): Type := Bij { bij_fwd:> A -> B; bij_bwd: B -> A; bijK: cancel bij_fwd bij_bwd; bijK': cancel bij_bwd bij_fwd }.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)