proposition: Lemma Hcodom : forall k : 'I_l.+2, 0 < k < l.+1 -> codom (u' k) \subset [:: p2; a[p1, p3] k].
proof: Proof. by move=> k kH; rewrite ffunE; apply/codom_liftr/cH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)