proposition: Lemma adj_injcp cp1 cp2 : cubic_prog cp1 -> {mono @injcp cp1 cp2 : x y / adj x y}.
proof: Proof. elim: cp1 cp2 => [|s cp1 IHcp] cp2 //=. case: s => // [n|||] cp_ok x y; rewrite IHcp //. - exact: adj_icpY. - exact: adj_icpH. exact: adj_icpU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)