proposition: Lemma adjunction_sumf_inl : fun_adjunction inl sumf f1 is_inl.
proof: Proof. apply: strict_adjunction closed_sumf_l _ _ _ => //; first exact: inl_inj. by apply/subsetP => -[u _|//]; rewrite codom_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)