proposition: Lemma cmergeK m n (c : configuration (m + n)) : cmerge (clshift c) (crshift c) = c.
proof: Proof. apply/ffunP=> i; rewrite !ffunE. by case: tsplitP => [] j iE; rewrite !ffunE /=; congr fun_of_fin; apply/val_eqP/eqP. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)