proposition: Lemma psi_aux_incr n l : l < (troot n).-1 -> (psi_aux l `[n] <= psi_aux l.+1 `[n])%R.
proof: Proof. move=> lLr. have dlLn : delta l.+2 <= n. rewrite -root_delta_le -subn_gt0. by rewrite -[l.+1]addn1 addnC subnDA subn_gt0 subn1. rewrite psi_auxE_lt psi_auxE_le. set s := \sum_(_ <- _ | _) _. have -> : [fset i in `[n] | l < troot i] = [fset i in `[n] | delta l.+1 <= i]. by apply/fsetP => i; rewrite !inE root_delta_le. have /(sint_sub n)-> : 0 <= delta l.+1 by apply: delta_le (_ : 0 <= l.+1). rewrite card_sint //. set c := n - _. rewrite expnS mulnAC [2 * _ * _]mulnC. rewrite mul2n mulnA muln2 -!addnn -[(_ + l.+1)%nat]addSnnS. rewrite mulnDl mulnDr prednDr ?(muln_gt0, expn_gt0) //. set x := 2 ^ _ * _. rewrite -[(_ + _ + s)%nat]addnA [(x + _)%nat]addnC. rewrite [((_ + _ * _)%:R)%R]natrD opprD addrA lerB //. rewrite lerBrDr [((_ + x)%:R)%R]natrD lerD //. rewrite ler_nat. rewrite mulnC leq_mul2l. rewrite -subSn; last first. apply: leq_trans (_ : delta l.+2 <= _); first by by apply: delta_le. by apply: leq_trans dlLn _. by rewrite ltn_subRL -addnS -deltaS (leq_trans dlLn) ?orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)