proposition: Lemma move_perfectl n (c1 c2 : configuration 3 n.+1) : c1 `--> c2 -> c1 ldisk != c2 ldisk -> ↓[c1] = `c[`p[c1 ldisk, c2 ldisk]].
proof: Proof. rewrite hmove_sym eq_sym opeg_sym. exact: move_perfectr. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)