proposition: Lemma psi_aux_psib l e : psi_auxb e <= l -> (psi_aux l e <= 0)%R.
proof: Proof. rewrite /psi_auxb; case: l => // l. rewrite ltnS /psi_aux geq_max => /andP[eLl maxLl]. rewrite mulSn -{2}[_ ^ _]prednK ?expn_gt0 // addSnnS. rewrite !natrD [(_%:R + _)%R]addrC opprD addrA addrK. rewrite subr_le0 ler_nat. apply: leq_trans (leqnSn _). apply: leq_trans (_ : #|`e| * 2 ^ l.+1 <= _); last first. by rewrite leq_mul2r eLl orbT. rewrite -fsum_nat_const. apply: leq_sum => i iIe. apply: leq_pexp2l => //. by apply geq_minr. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)