proposition: Lemma phi_gmin n : phi n = g n (gmin n).
proof: Proof. case: n => // n. rewrite {1}phi_modE /g /gmin. rewrite phi_deltaD; last by rewrite prednK // tmod_le. set x := troot _; set y := tmod _. rewrite phi_simpl //. rewrite doubleB doubleD -!muln2 -!mulnA -!expnSr !prednK //. have ->: n.+1 = delta x.-1 + x + y. by rewrite -{2}[x]prednK // -deltaS prednK // -tmodE. rewrite [_ + x + y]addnAC [_ + x]addnC addnK. rewrite {}/x {}/y. case: n => // [] [|n] //. rewrite phi_simpl //. rewrite -[_.-1]prednK // addSn. case: expn (expn_gt0 2 (troot n.+3)) => // u __. by rewrite addSn mulSn add0n -addSn addnAC. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)