proposition: Lemma gminE n : n = gmin n + troot n.
proof: Proof. case: n => //= n. rewrite {1}[n.+1]tmodE /gmin. case: troot (troot_gt0 (isT : 0 < n.+1)) => //= t _. by rewrite deltaS addnAC. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)