proposition: Lemma dsum_alphal_min_3 l n : S_[l] n.+1 = minn (S1 n.+1).*2 (S_[3 * l] n + l).
proof: Proof. rewrite {1}/dsum_alphaL /conv /= subnn muln0 addn0. congr (minn _ _). rewrite /dsum_alphaL /conv -bigmin_constD. apply: bigmin_ext => i iH; rewrite -addnA; congr (_ + _). rewrite -mulnAC -{3}[l]mul1n -mulnDl mulnC; congr (_ * _). rewrite -even_halfMl ?even_expn3_pred // -{4}[1]/(2./2). rewrite -even_halfD ?oddM ?even_expn3_pred //; congr (_./2). rewrite subSn // expnS -!subn1 mulnBr muln1 addn2 -!subSn ?subSS //. by rewrite ltnS -expnS (ltn_exp2l 0). by rewrite -expnS (leq_exp2l 1). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)