proposition: Lemma cnode_injcp cp1 cp2 : cubic_prog cp1 -> {in [predC cpring (cpmap cp2)], {mono @injcp cp1 cp2 : x y / cnode x y}}.
proof: Proof. move=> cp_ok x XN'x y; apply/idP/idP=> /iter_findex => [|<-]. elim: {x}(findex _ _ _) {-2}x XN'x => [|n IHn] x XN'x. by move/injcp_inj->. rewrite iterSr -node_injcp // cnode1; apply: IHn. by rewrite !inE mem_cpring -cnode1r -mem_cpring. elim: {x y}(findex _ _) {-3}x XN'x => // n IHn x XN'x. rewrite iterSr cnode1 -node_injcp //; apply: IHn. by rewrite !inE mem_cpring -cnode1r -mem_cpring. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)