proposition: Lemma sum_beta_S n l (a : configuration 4 n.+1) p : 1 < l -> sp a l p = \sum_(k < n) ((↓[a] k != p) * (α_[1] k).*2) + (a ord_max != p) * α_[l] n.
proof: Proof. move=> l_gt1; rewrite /sp. rewrite big_ord_recr /= /beta l_gt1 eqxx /=; congr (_ + _). apply: eq_bigr => i _; rewrite !ffunE; congr ((a _ != _) * _). by apply: val_inj. by rewrite eqn_leq [_ <= i]leqNgt ltn_ord andbF. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)