proposition: Lemma alphaLE l n : α_[l] n = fmerge (fun i : nat => (α i).*2) (fun i : nat => l * 3 ^ i) n.
proof: Proof. rewrite [LHS]delta_conv; last by apply: convex_3l. apply: fmerge_ext => i; first by rewrite delta_2S1. by rewrite delta_3l. by apply: convex_2S1. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)