proposition: Lemma option_sum_unit {A}: bij (option A) (A+unit).
proof: Proof. exists (fun x => match x with Some a => inl a | None => inr tt end) (fun x => match x with inl a => Some a | inr _ => None end). all: abstract (repeat case=>//). Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)