proposition: Lemma gmin_gt0 n : 1 < n -> 0 < gmin n.
proof: Proof. case: n => [|[|[|n _]]] //. apply: leq_trans (leq_addr _ _). have /troot_le : 3 <= n.+3 by []. rewrite -[troot 3]/(2). case: troot => //= m. by rewrite ltnS => /delta_le. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)