proposition: Lemma convex_2S1 : convex (fun i : nat => (S1 i).*2).
proof: Proof. split => [] i. by rewrite leq_double /dsum_alpha [X in _ <= X]big_ord_recr leq_addr. by rewrite !delta_2S1 leq_double; apply/ltnW/alpha_ltn. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)