proposition: Lemma S1_eq n : 0 < n -> S1 n = (S1 (n - (log3 (α n.-1)).+1)).*2 + (3 ^ (log3 (α n.-1)).+1).-1./2.
proof: Proof. case: n => // n _. apply: double_inj. rewrite doubleD div2K; last first. by rewrite -subn1 oddB ?expn_gt0 //= oddX orbT. rewrite -!mul2n predn_exp -mulnDr; congr (2 * _). have iLn : 3 ^ (log3 (α n)) <= α n < 3 ^ (log3 (α n)).+1. rewrite gtn_log3 leq_log3 //. by apply: alpha_gt0. by apply: sum_alpha_eq. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)