proposition: Lemma psi_aux_sint n : ((psi `[n])%:R)%R = psi_aux (troot n).-1 `[n].
proof: Proof. apply/eqP. rewrite eq_le psi_max andbT. case: (psiE `[n]) => l ->. have [E|E] := leqP (troot n).-1 l. rewrite -(subnK E). elim: (_ - _) => [|k IH] //. apply: le_trans IH. rewrite addSn. apply: psi_aux_decr => //. by rewrite leq_addl. rewrite -(subKn (ltnW E)). elim: (_ - l) => [|k IH]. by rewrite subn0. apply: le_trans IH. rewrite subnS. have [|E1] := leqP (troot n).-1 k. by rewrite -subn_eq0 => /eqP->. rewrite -{2}[_-_]prednK ?subn_gt0 //. apply: psi_aux_incr => //. case: _.-1 E1 => // u _; case: k => // k. apply: leq_trans (_ : u.+1.-1 < u.+1) => //. by rewrite ltnS -!subn1 leq_sub2r // leq_subr. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)