fact: Definition sumf {A B C D} (f: A -> B) (g: C -> D) (x: A+C): B+D := match x with inl a => inl (f a) | inr c => inr (g c) end.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)