fact: Definition pickle_Knm (i : KB) : nat := match i with inl (Ordinal k _) => k | inr (Ordinal k _) => n + k end.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)