proposition: Lemma gS n m : m.+1 < n -> g n m.+1 + 2 ^ (n - m.+1) = g n m + 2 ^ (troot m).+1.
proof: Proof. move=> H; rewrite /g !phi_modE. rewrite phi_simpl; last by rewrite troot_gt0. rewrite -[n - m]prednK; last first. by rewrite subn_gt0 (leq_trans _ H). rewrite -subnS expnS mul2n -[(2 ^ _).*2]addnn. have := troot_mod_case m. case/orP=> [/andP[/eqP H1 /eqP H2]|/and3P[/eqP H1 /eqP H2 /eqP H3]]. rewrite /g H1 H2 phi_simpl; last by rewrite -H1 troot_gt0. rewrite addnS mulSnr !addnA doubleD -!addnA; congr (_ + _). rewrite -mul2n -expnS addnC; congr (_ + _). by case: (_ ^ _). rewrite H1 H2 H3 addnn addn0 /=. set x := troot _; set y := n - _. rewrite doubleB [in RHS]addnAC -[(2 ^ _).*2]mul2n -expnS subnK; last first. rewrite expnS mul2n leq_double. by case: x => //= x; rewrite doubleS mulSnr addnA leq_addl. rewrite -[x.*2]muln2 -mulnA -expnS -addnA; congr (_ +_). by case: expn (expn_gt0 2 y). Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)