proposition: Lemma submodular_dsum_alphaL l n : S_[l] n.+1 + S_[l.+1] n <= S_[l] n + S_[l.+1] n.+1.
proof: Proof. rewrite -leq_subLR -addnBAC; last first. by have [daI _] := convex_dsum_alphaL l. rewrite -[_ - _]/(α_[l] _) addnC -leq_subRL; last first. by have [daI _] := convex_dsum_alphaL l.+1. rewrite -[_ - _]/(α_[l.+1] _). by apply: increasing_alphaL_l. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)