proposition: Lemma codom_cut (c : configuration k n) (s : seq (peg k)) : codom c \subset s -> codom (ccut c) \subset s.
proof: Proof. move=> H; apply/subsetP => i /mapP[j _ ->]. by rewrite ffunE; apply: (subsetP H); apply: codom_f. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)