proposition: Lemma concave_dsum_alphaL_l n : concave (fun l => S_[l] n).
proof: Proof. apply: concaveE (increasing_dsum_alphaL_l _) _ => i. rewrite {3}/dsum_alphaL /conv. pose f i x := (S1 x).*2 + i * ((3 ^ (n - x)).-1)./2. case: (eq_bigmin (f i.+1) n) => j ->. have -> : (f i.+1 j).*2 = f i j + f (i.+2) j. rewrite /f; set x := (S1 _).*2; set y := _./2. rewrite addnCA 2![in RHS]addnA addnn -[in RHS]addnA -mulnDl. by rewrite -addSnnS addnn -doubleMl -doubleD. apply: leq_add. by apply: bigmin_inf (leqnn _); rewrite -ltnS. by apply: bigmin_inf (leqnn _); rewrite -ltnS. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)