proposition: Lemma gmin_min n m : m < n -> g n (gmin n) <= g n m.
proof: Proof. move=> mLn. have [gLm|mLg] := leqP (gmin n) m. move: mLn; rewrite -(subnK gLm). elim: subn => // k IH H1. rewrite addSn (leq_trans (IH _) (gS_minr _ _)) ?leq_addl //. by apply: leq_trans H1; rewrite ltnS addSnnS leq_add2l. rewrite -(subKn (ltnW mLg)). elim: (gmin n - m) (leq_subr m (gmin n)) => [|k IH kLm]. by rewrite subn0. apply: leq_trans (IH (ltnW kLm)) _. rewrite -subSS subSn //. by rewrite gS_minl // -subSn // subSS leq_subr. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)