proposition: Lemma gS_minl n m : m < gmin n -> g n m.+1 <= g n m.
proof: Proof. case: n => // n mLg. have mLn : m < n. by rewrite -ltnS; apply: leq_trans (gmin_lt _). suff mtLm : m.+1 + troot m <= n. rewrite -(leq_add2r (2 ^ (n.+1 - m.+1))) (gS _) //. by rewrite leq_add2l leq_pexp2l // ltn_subRL. rewrite (leq_trans (_ : _ <= gmin n.+1 + troot m)) //. by rewrite leq_add2r. rewrite -ltnS -addnS. rewrite /gmin {3}[n.+1]tmodE addnAC leq_add2r. have : 0 < troot n.+1 by apply troot_gt0. case E : troot => [|t] _ //=. rewrite deltaS -E leq_add2l. by apply: gmin_root_lt. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)