proposition: Lemma delta_3l l i : delta (fun i : nat => l * ((3 ^ i).-1)./2) i = l * 3 ^ i.
proof: Proof. rewrite /delta -mulnBr -even_halfB //; try by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT. rewrite -predn_sub -subnS prednK ?expn_gt0 //. by rewrite expnS -[X in _ * ((_ - X))./2]mul1n -mulnBl mul2n doubleK. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)