proposition: Lemma leq_log3 n : 0 < n -> 3 ^ (log3 n) <= n.
proof: Proof. rewrite /log3; case: ex_minnP => [] [|m] //= nLm H nL. by rewrite leqNgt; apply/negP => /H; rewrite ltnn. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)