proposition: Lemma gmin_root_lt m n : m < gmin n -> troot m < troot n.
proof: Proof. move=> mLg. have nP : 0 < n by case: n mLg. case: leqP => //; rewrite leq_eqVlt => /orP[/eqP tnEtm| /ltn_root]; last first. by rewrite ltnNge (leq_trans _ (gmin_le _)) // ltnW. have /eqP tnEtg : troot n == troot (gmin n). by rewrite eqn_leq {1}tnEtm !troot_le // ?gmin_le // ltnW. have: tmod m < tmod (gmin n) by rewrite ltn_mod // -tnEtg. suff : tmod (gmin n) = 0 by move->. rewrite gmin_mod. have := gmin_root n; case: eqP => //. rewrite -tnEtg subn1 => _ F. have := ltnn (troot n). by rewrite -{2}(prednK (troot_gt0 nP)) -F leqnn. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)