proposition: Lemma gS_minr n m : gmin n <= m -> m.+1 < n -> g n m <= g n m.+1.
proof: Proof. move=> gLm mLn. suff mtLm : n <= m.+1 + (troot m).+1. rewrite -(leq_add2r (2 ^ (n - m.+1))) (gS _) //. by rewrite leq_add2l leq_pexp2l // leq_subLR. rewrite [n]gminE addSnnS leq_add //. apply: leq_trans (_ : (troot (gmin n)).+2 <= _). rewrite gmin_root; case: eqP; first by rewrite subn0 ltnW. by rewrite subn1; case: troot. by rewrite !ltnS troot_le. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)