proposition: Lemma main_cor p1 p2 n : p1 != p0 -> p2 != p0 -> p1 != p2 -> (S_[1] n).*2 <= `d[`c[p1, n],`c[p2, n]]_smove.
proof: Proof. move=> p1Dp0 p2Dp0 p1Dp2. rewrite eq_sym in p2Dp0. have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0. rewrite eq_sym in p2Dp0. pose u := [ffun i : 'I_2 => if i == 0 :> nat then `c[p1, n] else `c[p2, n]]. suff : (S_[1] n).*2 <= \sum_(i < 1) `d[u (inord i), u (inord i.+1)]_smove + \sum_(k < n) (u ord0 k != p1) * β_[n, 1] k + \sum_(k < n) (u ord_max k != p2) * β_[n, 1] k. rewrite big_ord_recr big_ord0 !ffunE /= inord_eq0 //= add0n. rewrite inordK //=. rewrite (eq_bigr (fun i : 'I_n => 0)) => [|i _]; last first. by rewrite !ffunE eqxx. rewrite -(big_mkord xpredT (fun=> 0)) sum_nat_const_nat muln0. rewrite (eq_bigr (fun i : 'I_n => 0)) => [|i _]; last first. by rewrite !ffunE eqxx. rewrite -(big_mkord xpredT (fun=> 0)) sum_nat_const_nat muln0. by rewrite !addn0. apply: (@main p1 p3 p2) => //. by rewrite eq_sym. by case=> [] []. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)