proposition: Lemma psi_aux_le_psi e1 e2 : (forall l, (psi_aux l e1 <= psi_aux l e2)%R) -> psi e1 <= psi e2.
proof: Proof. move=> H. pose e := maxn (psi_auxb e1) (psi_auxb e2). rewrite (psiE_leq (leq_maxl _ _ : _ <= e)). rewrite (psiE_leq (leq_maxr _ _ : _ <= e)). elim: e => [|e IH]; first by rewrite !big_ord0. by rewrite !big_ord_recr /= geq_max !leq_max IH /= rnz_ler // orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)