proposition: Lemma lhanoi3_nil_inv n (c1 c2 : _ _ n) : lhanoi3 c1 c2 = [::] -> c1 = c2.
proof: Proof. elim: n c1 c2 => [c1 c2 _|n IH c1 c2] /=; first by apply/ffunP=> [] []. case: eqP => [H | H] //=; last by case: lrel; case: map. rewrite -{2}[c1]cunliftrK -{3}[c2]cunliftrK. case: lhanoi3 (IH ↓[c1] ↓[c2]) => //= -> // _. by rewrite H. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)