proposition: Lemma S1_bigmin n : S1 n.+1 = \min_(i <= n) ((S1 i).*2 + (3 ^ (n.+1 - i)).-1./2).
proof: Proof. apply/eqP; rewrite eqn_leq; apply/andP; split; last first. rewrite S1_eq // -{2}(subKn (leq_log3_alpha n)). apply: bigmin_inf (leqnn _) => //. by rewrite leq_subLR addSnnS leq_addl. apply/bigmin_leqP => i iLn. rewrite -{1}(subKn (_ : i <= n.+1)); last by apply: ltnW. by apply/S1_leq/leq_subr. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)