fact: Definition option2x {A}: option (option A) -> option (option A) := fun x => match x with Some (Some a) => Some (Some a) | Some None => None | None => Some None end.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)