proposition: Lemma lim_dsum_alphaL_l l n : (S1 n).*2 <= l -> S_[l] n = (S1 n).*2.
proof: Proof. move=> S1Ll; apply/eqP. rewrite /dsum_alphaL /conv eqn_leq; apply/andP; split. apply: bigmin_inf (_ : _ n <= _) => //. by rewrite subnn muln0 addn0. apply/bigmin_leqP => i. case: ltngtP => // [iLn _|-> _]; last apply: leq_addr. apply: leq_trans S1Ll _. apply: leq_trans (leq_addl _ _). rewrite -{1}[l]muln1 leq_mul2l (half_leq (_ : 2 <= _)) ?orbT //. by rewrite -ltnS prednK ?expn_gt0 // (@leq_exp2l _ 1) // subn_gt0. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)