proposition: Lemma sum_alpha_diffE n (f : configuration 4 n.+1) (p1 p2 : peg 4) v1 v2 : 1 < v1 -> 1 < v2 -> p1 != p2 -> codom f \subset [:: p1; p2] -> sp f v1 p1 + sp f v2 p2 <= (S_[1] n).*2 + α_[maxn v1 v2] n.
proof: Proof. move=> v1_gt1 v2_gt1 p1Dp2 cH. rewrite !sum_beta_S //. rewrite -addnA -addnCA addnC !addnA -addnA leq_add //. rewrite leq_eqVlt; apply/orP; left; apply/eqP. rewrite -addnn !dsum_alphaLE -!big_split /=; apply: eq_bigr => i _. rewrite !ffunE; set v := trshift _ _. have /subsetP := cH => /(_ (f v) (codom_f _ _)). rewrite !inE addnn. case: eqP => /= x1; case: eqP => /= x2; rewrite ?(mul1n, add0n, addn0) //. by move/eqP: x2; rewrite x1 (negPf p1Dp2). have /subsetP/(_ (f ord_max) (codom_f _ _)) := cH. rewrite !inE. case: eqP => /= x1; case: eqP => /= x2 // _; rewrite ?(mul1n, add0n, addn0) //; apply: (increasingE (increasing_alphaL_l _)). by apply: leq_maxr. by apply: leq_maxl. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)