proposition: Lemma psi_sub e1 e2 : e1 `<=` e2 -> psi e1 <= psi e2.
proof: Proof. move=> e1Se2. rewrite (psiE_leq (leq_maxl (psi_auxb e1) (psi_auxb e2))). rewrite (psiE_leq (leq_maxl (psi_auxb e2) (psi_auxb e1))). rewrite maxnC. elim/big_ind2: _ => // [x1 x2 y1 y2 x2Lx1 y2Ly1 | i _]. rewrite geq_max (leq_trans x2Lx1 (leq_maxl _ _)). by rewrite (leq_trans y2Ly1 (leq_maxr _ _)). apply: rnz_ler. by apply: psi_aux_sub. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)