proposition: Lemma phi_modSE n : phi n.+1 = 1 + (troot n + tmod n) * 2 ^ (troot n).
proof: Proof. rewrite phi_modE. have /orP[/andP[/eqP-> /eqP->]| /and3P[/eqP->/eqP->/eqP]->] := troot_mod_case n. by rewrite addnS mulSn addnCA [2 ^ _ + _]addnC addnK. rewrite addn0 mulSn addnCA [2 ^ _ + _]addnC addnK. by rewrite expnS addnn -mul2n mulnCA mulnA. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)