proposition: Lemma S1_leq n i : i <= n -> S1 n <= (S1 (n - i)).*2 + (3 ^ i).-1./2.
proof: Proof. move=> iLn. rewrite -leq_double doubleD div2K; last first. by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT. rewrite -!mul2n predn_exp. rewrite -mulnDr leq_mul2l /=. by apply: sum_alpha_leq. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)