proposition: Lemma cpmask1 cp i : i < cpksize cp -> config_prog cp -> cpmask (cfmask1 cp i) cp = [:: nth (cpmap cp : cpmap cp) (cpker cp) i].
proof: Proof. move=> lt_i_cp cp_ok; move: (cpmap cp : cpmap cp) lt_i_cp => /= x0. rewrite mask_false cat0s -size_cpker {cp_ok}// -{2}[i]addn0 /mkseq. elim: (cpker cp) 0 i => // [x p IHp] j [|i] /= lt_i_cp. rewrite add0n eqxx -addn1; congr (_ :: _). elim: p 0 {x IHp lt_i_cp} => //= [x p IHp] i. by rewrite -addnS IHp -{2}[j]addn0 eqn_add2l. by rewrite -{1}[j]add0n eqn_add2r /= addSnnS IHp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)