proposition: Lemma adjunction_sumf_inr : fun_adjunction inr sumf f2 [predC is_inl].
proof: Proof. apply: strict_adjunction _ _ _ => //; try exact: inr_inj. by apply/predC_closed/closed_sumf_l. 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)