proposition: Lemma cdisjointP m n (c1 : configuration m) (c2 : configuration n) : reflect (forall i j, c1 i != c2 j) (cdisjoint c1 c2).
proof: Proof. apply: (iffP forallP) => [H i j| H i]. by move/forallP : (H i); apply. by apply/forallP=> j; apply: H. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)