proposition: Lemma gmin_root n : troot (gmin n) = troot n - (tmod n != troot n).
proof: Proof. have [/eqP mEt|mDt] := boolP (tmod n == troot n). rewrite /gmin -mEt subn0. by case: tmod => //= t; rewrite -deltaS troot_delta. have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le. rewrite subn1. apply/eqP; rewrite /gmin trootE. case: n {mDt}mLt => // [] [|] // n mLt. case: troot mLt => //= t mLt. by rewrite leq_addr deltaS ltn_add2l. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)