proposition: Lemma convex_3l l : convex (fun i : nat => l * ((3 ^ i).-1)./2).
proof: Proof. split => [] i. rewrite leq_mul2l half_leq ?orbT //. by apply: leq_pred2; rewrite leq_exp2l. by rewrite !delta_3l leq_mul2l leq_exp2l // leqnSn orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)