proposition: Lemma s2f_cut (c : configuration k n) (p : disk k) : s2f ([set i | c i == p] :&: isO n t) = s2f [set i | ccut c i == p].
proof: Proof. apply/fsetP=> /= i. apply/imfsetP/imfsetP => [] /= [j]; rewrite !inE. case/andP => cjEp jLt ->. by exists (Ordinal jLt); rewrite //= inE !ffunE ordinalK. rewrite !ffunE => cjEp ->; exists (widen_ord tLn j) => //=. by rewrite !inE /= cjEp /=. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)