proposition: Lemma edge_injcp cp1 cp2 : cubic_prog cp1 -> {morph @injcp cp1 cp2 : x / edge x}.
proof: Proof. by elim: cp1 cp2 => [|s cp1 IHcp] cp2 //; case: s => //= * x; rewrite -IHcp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)