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