proposition: Lemma gmin_mod n : tmod (gmin n) = (tmod n != troot n) * tmod n.
proof: Proof. have [/eqP mEt|mDt] := boolP (tmod n == troot n). rewrite mul0n /gmin -mEt. case: (tmod n) => // t. by rewrite -deltaS tmod_delta. have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le. by rewrite mul1n /tmod {1}/gmin gmin_root mDt subn1 addnC addnK. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)